---

Step * of Lemma wfd-tree-rec_wf

∀[X,T:Type]. ∀[b:X]. ∀[F:(T ⟶ X) ⟶ X]. ∀[t:wfd-tree(T)].  (wfd-tree-rec(b;r.F[r];t) ∈ X)
BY
{ (Unfold `wfd-tree` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[X,T:Type].  \mforall{}[b:X].  \mforall{}[F:(T  {}\mrightarrow{}  X)  {}\mrightarrow{}  X].  \mforall{}[t:wfd-tree(T)].    (wfd-tree-rec(b;r.F[r];t)  \mmember{}  X)


By

---

Latex:
(Unfold  `wfd-tree`  0  THEN  ProveWfLemma)

---

Home Index