Require Import Arith Lia.
Require Import Bool.
Require Import List.
Import ListNotations.

Inductive value: Type :=
| CtorVal (ctor: nat) (args: list value)
.

Definition foldl2 {X Y Z: Type} (f: X -> Y -> Z -> Z) :=
   fix foldl2 (z: Z) (xs: list X) (ys: list Y) : Z :=
      match xs with
      | [] => z
      | x :: xs' =>
           match ys with
           | [] => z
           | y :: ys' =>
                foldl2 (f x y z) xs' ys'
           end
      end.

Fixpoint value_eqb (a b: value) :=
   match a with
   | CtorVal ctora argsa =>
        match b with
        | CtorVal ctorb argsb =>
             (ctora =? ctorb) && (length argsa =? length argsb) &&
                 foldl2 (fun arga argb z => z && value_eqb arga argb) true argsa argsb
        end
   end.