fact: Definition smAlpha'' : lnatTrans (lord_functor_comp (strict2laxFunc (lad_L tradj1)) Kl_Lfunc_filled) (lord_functor_comp (strict2laxFunc (ord_functor_id I)) (strict2laxFunc (lad_L tradj2))) := lnatTrans_comp PPre_smAlpha'' post_smAlpha''.
imports: Coq(Relation_Definitions) Relational(OrderEnrichedCategory) Mon(SPropBase) mathcomp(all_ssreflect boolp) Crypt(Axioms OrderEnrichedRelativeAdjunctions LaxFunctorsAndTransf LaxMorphismOfRelAdjunctions)