proposition: Lemma zip_app : forall (A B : Set)(lsa1 lsa2 : list A)(lsb1 lsb2 : list B), length lsa1 = length lsb1 -> length lsa2 = length lsb2 -> (zip lsa1 lsb1) ++ (zip lsa2 lsb2) = (zip (lsa1 ++ lsa2) (lsb1 ++ lsb2)).
proof: Proof. induction lsa1; destruct lsb1; destruct lsa2; destruct lsb2; intuition; simpl in *; try lia. repeat rewrite app_nil_r. trivial. f_equal. rewrite <- IHlsa1. simpl. trivial. lia. simpl. lia. Qed.
imports: FCF.FCF Permutation