proposition: Lemma forall2b_Forall2 : forall {A B: Type} (F : A -> B -> bool) l1 l2, forall2b F l1 l2 = true <-> Forall2 (fun x y => F x y = true) l1 l2.
proof: Proof. induction l1 ; simpl. - destruct l2. split ; auto. intuition try congruence. inv H. - destruct l2. split ; try discriminate. intros. inv H. rewrite andb_true_iff. rewrite IHl1. intuition. inv H ; auto. inv H ;auto. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List