---

Step * of Lemma fun_exp-id

∀[n:ℕ]. ∀[x:Top].  (λi.i^n x ~ x)
BY
{ (InductionOnNat THEN Reduce 0 THEN Try (Complete (Auto)) THEN ParallelLast) }

1
1. n : ℤ
2. 0 < n
3. ∀[x:Top]. (λi.i^n - 1 x ~ x)
4. [x] : Top
5. λi.i^n - 1 x ~ x
⊢ λi.i^n x ~ x

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:Top].    (\mlambda{}i.i\^{}n  x  \msim{}  x)


By

---

Latex:
(InductionOnNat  THEN  Reduce  0  THEN  Try  (Complete  (Auto))  THEN  ParallelLast)

---

Home Index