proposition: Lemma foo : forall (I: A -> Prop) acc, I acc -> (forall a b1 b2, I a -> I (f a b1 b2)) -> forall xs ys, I (fold_left2 xs ys acc).
proof: Proof. intros I acc H0 H1 xs. revert acc H0. induction xs as [ | a xs IHxs]; intros acc H. simpl. auto. intros [ | b ys]. + simpl. exact H. + simpl. apply IHxs, H1. exact H. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance