fact: Hypothesis (StrucIsoPres' : forall (A : I) (Y : C1) (f : C1 ⦅ J1 (Lflat A) ; Y ⦆), lofmap (strict2laxFunc KC) f = (natIso_sym (Chi_RJLflat_2) ⟨ A, strict2laxFunc KC Y ⟩) ∙1 ((smBeta' Y ∙ ofmap KC ((Chi_RJLflat_1 ⟨ A, Y ⟩) ∙1 f)) ∙ chi A) ∙ smAlpha' A).
imports: Coq(Relation_Definitions) Relational(OrderEnrichedCategory) Mon(SPropBase) mathcomp(all_ssreflect boolp) Crypt(Axioms OrderEnrichedRelativeAdjunctions LaxFunctorsAndTransf LaxMorphismOfRelAdjunctions)