+ apply roundtrip_lemma.
+
+ apply if_inv.
+ set (step1_niso s1 (smme_mee s2) s2 r0) as q'.
+ apply if_inv in q'.
+ eapply if_comp.
+ eapply if_comp; [ idtac | apply q' ].
+ eapply if_comp.
+ apply (if_associativity
+ (RestrictToImage r0)
+ (R' s1 s2 r0 >>>> ff_functor_section_functor me_homfunctor me_full me_faithful)
+ (HomFunctor (senr_c s2) (senr_c_i s2))).