---

Step * 1 of Lemma comp_id_l


∀[A,B:Type]. ∀[f:A ⟶ B].  ((Id o f) = f ∈ (A ⟶ B))
BY
{ (Unfolds ``identity compose`` 0 THEN Auto) }

---

Latex:

---

Latex:

\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].    ((Id  o  f)  =  f)


By

---

Latex:
(Unfolds  ``identity  compose``  0  THEN  Auto)

---

Home Index