---

Step * 1 of Lemma wfd-tree-induction


1. [T] : Type
2. P : wfd-tree(T) ⟶ ℙ
3. P[Wsup(tt;⋅)]
4. ∀f:T ⟶ wfd-tree(T). ((∀b:T. P[f b]) ⇒ P[Wsup(ff;f)])
5. x : 0 = 0 ∈ ℤ
6. f : Void ⟶ wfd-tree(T)
7. ∀b:Void. P[f b]
⊢ P[Wsup(tt;f)]
BY
{ (NthHypEq 3 THEN EqCD THEN Auto THEN Unfold `wfd-tree` 0 THEN EqCD THEN Auto THEN Ext THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  wfd-tree(T)  {}\mrightarrow{}  \mBbbP{}
3.  P[Wsup(tt;\mcdot{})]
4.  \mforall{}f:T  {}\mrightarrow{}  wfd-tree(T).  ((\mforall{}b:T.  P[f  b])  {}\mRightarrow{}  P[Wsup(ff;f)])
5.  x  :  0  =  0
6.  f  :  Void  {}\mrightarrow{}  wfd-tree(T)
7.  \mforall{}b:Void.  P[f  b]
\mvdash{}  P[Wsup(tt;f)]


By

---

Latex:
(NthHypEq  3
  THEN  EqCD
  THEN  Auto
  THEN  Unfold  `wfd-tree`  0
  THEN  EqCD
  THEN  Auto
  THEN  Ext
  THEN  All  Reduce
  THEN  Auto)

---

Home Index