proposition: Lemma map_snd_zip : forall (A B : Set)(lsa : list A)(lsb : list B), length lsa = length lsb -> map (fun p => snd p) (zip lsa lsb) = lsb.
proof: Proof. induction lsa; intuition; simpl in *. destruct lsb; simpl in *; congruence. destruct lsb; simpl in *; try lia. f_equal. eauto. Qed.
imports: FCF.FCF Permutation