---

Step * of Lemma stump-bars

∀T:Type. ∀t:wfd-tree(T). ∀alpha:ℕ ⟶ T.  ∃n:ℕ. (¬↑(stump(t) n alpha))
BY
{ ((D 0 THENA Auto)
   THEN (BLemma `wfd-tree-induction` THENA Auto)
   THEN Unfold `stump` 0
   THEN Reduce 0
   THEN Try (Fold `stump` 0)
   THEN Auto) }

1
1. T : Type
2. alpha : ℕ ⟶ T
⊢ ∃n:ℕ. (¬False)

2
1. T : Type
2. f : T ⟶ wfd-tree(T)
3. ∀b:T. ∀alpha:ℕ ⟶ T.  ∃n:ℕ. (¬↑(stump(f b) n alpha))
4. alpha : ℕ ⟶ T
⊢ ∃n:ℕ. (¬↑if (n =z 0) then tt else stump(f (alpha 0)) (n - 1) (λi.(alpha (i + 1))) fi )

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}t:wfd-tree(T).  \mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  T.    \mexists{}n:\mBbbN{}.  (\mneg{}\muparrow{}(stump(t)  n  alpha))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (BLemma  `wfd-tree-induction`  THENA  Auto)
  THEN  Unfold  `stump`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `stump`  0)
  THEN  Auto)

---

Home Index