---

Step * of Lemma fun_exp_compose

∀[T:Type]. ∀[n:ℕ]. ∀[h,f:T ⟶ T].  ((f^n o h) = primrec(n;h;λi,g. (f o g)) ∈ (T ⟶ T))
BY
{ (((RepeatFor 2 (D 0 THENA Auto) THEN NatInd (-1)) THEN Unfold `fun_exp` 0) THEN Reduce 0) }

1
1. T : Type
2. n : ℤ
⊢ ∀[h,f:T ⟶ T].  (((λx.x) o h) = h ∈ (T ⟶ T))

2
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀[h,f:T ⟶ T].  ((f^n - 1 o h) = primrec(n - 1;h;λi,g. (f o g)) ∈ (T ⟶ T))
⊢ ∀[h,f:T ⟶ T].  ((primrec(n;λx.x;λi,g. (f o g)) o h) = primrec(n;h;λi,g. (f o g)) ∈ (T ⟶ T))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[h,f:T  {}\mrightarrow{}  T].    ((f\^{}n  o  h)  =  primrec(n;h;\mlambda{}i,g.  (f  o  g)))


By

---

Latex:
(((RepeatFor  2  (D  0  THENA  Auto)  THEN  NatInd  (-1))  THEN  Unfold  `fun\_exp`  0)  THEN  Reduce  0)

---

Home Index