fact: Fixpoint forallb2 {A : Type} (f : A -> A -> bool) (l1 l2 :list A) : bool := match l1, l2 with | nil, nil => true | cons h1 t1, cons h2 t2 => f h1 h2 && forallb2 f t1 t2 | _, _ => false end.
imports: QuickChick(QuickChick) ZArith List QuickChick.ifcbasic(Machine)