+ eapply if_comp.
+ idtac.
+ apply (if_associativity (garrow_functor s1 s0 r) (RepresentableFunctor s0 (mon_i s0)) (garrow_functor s0 s2 r0)).
+ Set Printing Coercions.
+ idtac.
+ unfold garrow_functor at 1.
+ unfold step2_functor at 1.
+ set (roundtrip_lemma'
+ (RepresentableFunctor (enr_c (smme_e s0)) (me_i (smme_mon s0)))
+ (ffme_mf_full (smme_mee s0)) (ffme_mf_faithful (smme_mee s0))
+ (step1_functor (smme_see s1) (smme_mee s0) r)
+ ) as q.
+ set (if_respects
+ (G0:=garrow_functor (smme_see s0) (smme_mee s2) r0)
+ (G1:=garrow_functor (smme_see s0) (smme_mee s2) r0)
+ q (if_id _)) as q'.
+ apply (if_comp q').
+ Unset Printing Coercions.
+ clear q' q.
+ unfold garrow_functor at 2.
+ unfold garrow_functor at 1.
+ eapply if_comp.
+ eapply if_inv.
+ apply (if_associativity _ (step1_functor s0 s2 r0) (step2_functor s2)).
+ apply (if_respects
+ (G0:=step2_functor s2)
+ (G1:=step2_functor s2)); [ idtac | apply if_id ].
+ apply step1_lemma.