proposition: Lemma subst_interchange_law_gen_instantiated {X Y Z : sortToC} (f : sortToC⟦X,M (Y ⊕ Z)⟧) (g : sortToC⟦Y, M Z⟧) : monadSubstGen_instantiated f · monadSubstGen_instantiated g = mexch_instantiated · monadSubstGen_instantiated (g · mweak_instantiated) · monadSubstGen_instantiated (f · monadSubstGen_instantiated g).
proof: Proof. apply subst_interchange_law_gen. Qed.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.PartD UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.Combinatorics.Lists UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Chains.All UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.Groupoids