proposition: Lemma subst_interchange_law_instantiated {t s: sort} {Γ: HSET_over_sort} (NN: HSET_over_sort⟦constHSET_slice t, T (constHSET_slice s ⊕ Γ)⟧) (LL: HSET_over_sort⟦constHSET_slice s, T Γ⟧): (monadSubstGen_instantiated _ NN) · (monadSubstGen_instantiated _ LL) = (mexch_instantiated (Γ1:=constHSET_slice t) (Γ2:=constHSET_slice s) (Γ3:=Γ)) · (monadSubstGen_instantiated _ (LL · (mweak_instantiated _))) · (monadSubstGen_instantiated _ (NN · (monadSubstGen_instantiated _ LL))).
proof: Proof. apply subst_interchange_law_gen. Qed.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Slice UniMath.CategoryTheory.slicecat