proposition: Theorem concatEquivalence: forall {T: Type} i (x: list (list T)), pmconcat i x = mconcat x.
proof: Proof. intros. funelim (pmconcat i x). reflexivity. rewrite H. now rewrite <- (morphism_distribution mconcat). Qed.
imports: Arith Coq.Classes.DecidableClass Coq.Program.Wf List Lia PeanoNat Program Equations(Equations)