proposition: Theorem combine_app : forall (A B : Type) (lsa1 lsa2 : list A) (lsb1 lsb2 : list B), length lsa1 = length lsb1 -> combine (lsa1 ++ lsa2) (lsb1 ++ lsb2) = (combine lsa1 lsb1) ++ (combine lsa2 lsb2).
proof: Proof. induction lsa1; destruct lsb1; intros; simpl in *; try discriminate. reflexivity. f_equal. eapply IHlsa1. lia. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms