fact: Definition smBeta'' : lnatTrans (lord_functor_comp (strict2laxFunc (lad_R tradj1)) (strict2laxFunc KC)) (lord_functor_comp Kl_Lfunc_filled (strict2laxFunc (lad_R tradj2))) := lnatTrans_comp PPre_smBeta'' post_smBeta''.
imports: Coq(Relation_Definitions) Relational(OrderEnrichedCategory) Mon(SPropBase) mathcomp(all_ssreflect boolp) Crypt(Axioms OrderEnrichedRelativeAdjunctions LaxFunctorsAndTransf LaxMorphismOfRelAdjunctions)