---

Step * of Lemma p-compose-id

∀[A,B:Type]. ∀[f:A ⟶ (B + Top)].  (f o p-id() = f ∈ (A ⟶ (B + Top)))
BY
{ (Auto THEN RepUR ``p-compose p-id can-apply do-apply`` 0 THEN Ext THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  (B  +  Top)].    (f  o  p-id()  =  f)


By

---

Latex:
(Auto  THEN  RepUR  ``p-compose  p-id  can-apply  do-apply``  0  THEN  Ext  THEN  Reduce  0  THEN  Auto)

---

Home Index