proposition: Lemma unzip_zip_inv : forall (A B : Set)(lsa : list A)(lsb : list B), length lsa = length lsb -> unzip (zip lsa lsb) = (lsa, lsb).
proof: Proof. induction lsa; destruct lsb; intuition; simpl in *; try lia. unfold unzip in *. simpl. assert ((map (fst (B:=B)) (zip lsa lsb), map (snd (B:=B)) (zip lsa lsb)) = (lsa, lsb)). eapply IHlsa. lia. repeat f_equal. congruence. congruence. Qed.
imports: FCF.FCF Permutation