+ eapply if_comp.
+ apply (if_associativity (R' smme smme x) (ff_functor_section_functor me_homfunctor me_full me_faithful)
+ (HomFunctor (senr_c smme) (senr_c_i smme))).
+ set (roundtrip_lemma (me_full(MonicEnrichment:=smme_mee smme))) as q.
+ set (R' smme smme x) as f.
+ set (me_faithful(MonicEnrichment:=smme_mee smme)) as ff.
+ unfold HomFunctor_fullimage in f.
+ unfold mf_F in f.
+ set (q ff _ _ (FullImage x) _ f) as q'.
+ unfold me_homfunctor in q'.
+ exact q'.