---

Step * 1 of Lemma p-fun-exp-compose


1. T : Type
2. n : ℤ
⊢ ∀[h,f:T ⟶ (T + Top)].  (p-id() o h = h ∈ (T ⟶ (T + Top)))
BY
{ (Auto THEN BLemma `p-id-compose` THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbZ{}
\mvdash{}  \mforall{}[h,f:T  {}\mrightarrow{}  (T  +  Top)].    (p-id()  o  h  =  h)


By

---

Latex:
(Auto  THEN  BLemma  `p-id-compose`  THEN  Auto)

---

Home Index