---

Step * of Lemma ident_trans_ap_lemma

No Annotations
∀A,F,D,C:Top.  (identity-trans(C;D;F) A ~ cat-id(D) (F A))
BY
{ (RepUR ``identity-trans`` 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}A,F,D,C:Top.    (identity-trans(C;D;F)  A  \msim{}  cat-id(D)  (F  A))


By

---

Latex:
(RepUR  ``identity-trans``  0  THEN  Auto)

---

Home Index