+ set (RepresentableFunctor s0 K) as a in *.
+ set (reification_rstar_f X) as a' in *.
+ set (reification_rstar_f X0) as x in *.
+ set (reification_r X K) as b in *.
+ set (reification_r X0 (mon_i s1)) as c in *.
+ set (RepresentableFunctor s2 (mon_i s2)) as c' in *.
+ set (RepresentableFunctor s1 (mon_i s1)) as b' in *.
+ apply (ni_comp(F2:=b >>>> (b' >>>> x))).
+ apply (@ni_respects _ _ _ _ _ _ _ _ _ _ b _ b _ (c >>>> c') _ (b' >>>> x)).
+ apply ni_id.
+ apply comm2.
+ eapply ni_comp.
+ eapply ni_inv.
+ apply (ni_associativity b b' x).
+ eapply ni_inv.
+ eapply ni_comp.
+ eapply ni_inv.
+ apply (ni_associativity a a' x).
+ apply (@ni_respects _ _ _ _ _ _ _ _ _ _ (a >>>> a') _ (b >>>> b') _ x _ x).
+ apply ni_inv.
+ apply comm1.
+ apply ni_id.