---

Step * of Lemma p-fun-exp-one

∀[A:Type]. ∀[f:A ⟶ (A + Top)].  (f^1 = f ∈ (A ⟶ (A + Top)))
BY
{ ((RepUR ``p-fun-exp`` 0 THEN Auto) THEN BLemma `p-compose-id` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  (A  +  Top)].    (f\^{}1  =  f)


By

---

Latex:
((RepUR  ``p-fun-exp``  0  THEN  Auto)  THEN  BLemma  `p-compose-id`  THEN  Auto)

---

Home Index