proposition: Lemma In_zip : forall (A B : Set)(a : A)( b : B) lsa lsb, In (a, b) (zip lsa lsb) -> In a lsa /\ In b lsb.
proof: Proof. induction lsa; intuition; simpl in *. intuition. destruct lsb. inversion H. simpl in H. intuition. pairInv. intuition. right. eapply IHlsa. eauto. destruct lsb. inversion H. simpl in *. intuition. pairInv. intuition. right. eapply IHlsa. eauto. Qed.
imports: FCF.FCF Permutation