- set (invert_reif _ f') as q.
- destruct q; subst.
- apply if_id.
- simpl in *.
- destruct H0; subst.
- simpl in *.
- unfold garrow_functor.
- unfold step2_functor.
- apply (if_comp H).
- clear H.
- apply (if_comp (@step1_niso _ smme _ _ smme x)).
- apply if_inv.
- apply (@roundtrip_lemma _ smme _ _ smme x).
+ set (invert_reif _ f') as q.
+ destruct q; subst.
+ apply if_id.
+
+ simpl in *.
+ destruct H0; subst.
+ simpl in *.
+ unfold garrow_functor.
+ unfold step2_functor.
+ apply (if_comp H).
+ clear H.
+ eapply if_comp.
+ apply (step1_niso smme (smme_mee smme) (smme_mon smme) x).
+ apply if_inv.
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage x) (R' smme smme x) (FullImage_InclusionFunctor _)).
+ apply if_inv.
+ eapply if_comp.
+ apply (if_associativity (RestrictToImage x) ((R' smme smme x >>>>
+ ff_functor_section_functor me_homfunctor me_full me_faithful))
+ (HomFunctor (senr_c smme) (senr_c_i smme))).
+ apply (if_respects (RestrictToImage x) (RestrictToImage x)).
+ apply (if_id (RestrictToImage x)).
+ unfold mf_F.
+ 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'.
+