proposition: Theorem Forall2_all_In : forall (A B : Type)(lsa : list A)(lsb : list B) (P : A -> B -> Prop), (length lsa = length lsb) -> (forall a b, In a lsa -> In b lsb -> P a b) -> Forall2 P lsa lsb.
proof: Proof. induction lsa; destruct lsb; intuition idtac; simpl in *. econstructor. discriminate. discriminate. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation