fact: Fixpoint eqbList(A : Set)(eqd : EqDec A)(ls1 ls2 : list A) := match ls1 with | nil => match ls2 with | nil => true | _ :: _ => false end | a1 :: ls1' => match ls2 with | nil => false | a2 :: ls2' => (eqb a1 a2) && (eqbList _ ls1' ls2') end end.
imports: Bvector Arith