---

Step * 1 of Lemma fun_exp_compose


1. T : Type
2. n : ℤ
⊢ ∀[h,f:T ⟶ T].  (((λx.x) o h) = h ∈ (T ⟶ T))
BY
{ (((Auto THEN FunExt) THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbZ{}
\mvdash{}  \mforall{}[h,f:T  {}\mrightarrow{}  T].    (((\mlambda{}x.x)  o  h)  =  h)


By

---

Latex:
(((Auto  THEN  FunExt)  THEN  Reduce  0)  THEN  Auto)

---

Home Index