---

Step * of Lemma wfd_tree_rec_node_lemma

∀F,f,F,b:Top.  (wfd-tree-rec(b;r.F[r];Wsup(ff;f)) ~ F[λx.wfd-tree-rec(b;r.F[r];f x)])
BY
{ (UnivCD THENA Auto) }

1
1. F : Top@i
2. f : Top@i
3. F1 : Top@i
4. b : Top@i
⊢ wfd-tree-rec(b;r.F1[r];Wsup(ff;f)) ~ F1[λx.wfd-tree-rec(b;r.F1[r];f x)]

---

Latex:

---

Latex:
\mforall{}F,f,F,b:Top.    (wfd-tree-rec(b;r.F[r];Wsup(ff;f))  \msim{}  F[\mlambda{}x.wfd-tree-rec(b;r.F[r];f  x)])


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index