proposition: Lemma in_zip_swap : forall (A B : Set)(lsa : list A)(lsb : list B) a b, length lsa = length lsb -> In (a, b) (zip lsa lsb) -> In (b, a) (zip lsb lsa).
proof: Proof. induction lsa; destruct lsb; intuition; simpl in *; try lia. intuition. pairInv. intuition. Qed.
imports: FCF.FCF Permutation