proposition: Lemma zip_length : forall (A B : Set)(lsa : list A)(lsb : list B), length lsa = length lsb -> length (zip lsa lsb) = length lsa.
proof: Proof. induction lsa; intuition; simpl in *. destruct lsb; simpl in *. discriminate. f_equal. eapply IHlsa. lia. Qed.
imports: FCF.FCF Permutation