- (*
- Lemma step1_lemma (s0 s1 s2:SmallSMMEs.SMMEs)(r01:Reification s0 s1 (me_i s1))(r12:Reification s1 s2 (me_i s2)) :
- ∀A : enr_v_mon s0,
- garrow_fobj' s1 s2 r12 (ehom(ECategory:=s1) (me_i s1) (garrow_fobj s0 s1 r01 A))
- ≅ garrow_fobj' s0 s2 (compose_reifications s0 s1 s2 r01 r12) A.
- *)
-