proposition: Lemma prop_forallb2: forall {A B} {f: A -> B -> bool} l1 l2, forallb2 f l1 l2 = true -> length l1 = length l2.
proof: Proof. intros A B f l1. induction l1 as [ | xl1 xsl1 IHl1]. - intros. simpl in H. case l2 in *. easy. now contradict H. - intros. simpl in H. case l2 in *. now contradict H. simpl. rewrite andb_true_iff in H. destruct H. apply IHl1 in H0. now rewrite H0. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance