---

Step * 1 of Lemma stump'-inductive


1. T : Type
⊢ stump'(Wsup(tt;⋅))
= wfd-tree-rec(λn,s. (n =z 0);r.λn,s. if (n =z 0) then ff else r (s 0) (n - 1) (λi.(s (i + 1))) fi ;Wsup(tt;⋅))
∈ (n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹)
BY
{ (RepUR ``stump\' stump empty-wfd-tree`` 0 THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
\mvdash{}  stump'(Wsup(tt;\mcdot{}))
=  wfd-tree-rec(\mlambda{}n,s.  (n  =\msubz{}  0);r.\mlambda{}n,s.  if  (n  =\msubz{}  0)
                                                                  then  ff
                                                                  else  r  (s  0)  (n  -  1)  (\mlambda{}i.(s  (i  +  1)))
                                                                  fi  ;Wsup(tt;\mcdot{}))


By

---

Latex:
(RepUR  ``stump\mbackslash{}'  stump  empty-wfd-tree``  0  THEN  EqCD  THEN  Auto)

---

Home Index