fact: Fixpoint forall2b (l1 : list A) (l2 : list B) : bool := match l1 , l2 with | nil , nil => true | e1::l1', e2::l2' => F e1 e2 && forall2b l1' l2' | _ , _ => false end.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List