proposition: Theorem combine_cons : forall (A B : Type) a1 (lsa2 : list A) b1 (lsb2 : list B), combine (a1 :: lsa2) (b1 ::lsb2) = (a1, b1) :: (combine lsa2 lsb2).
proof: Proof. intuition idtac. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms