---

Step * of Lemma diverge_wf

∀[T:Type]. (diverge() ∈ bar-base(T))
BY
{ (ProveWfLemma THEN Unfold `bar-base` 0 THEN BLemma `fix_wf_corec` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  (diverge()  \mmember{}  bar-base(T))


By

---

Latex:
(ProveWfLemma  THEN  Unfold  `bar-base`  0  THEN  BLemma  `fix\_wf\_corec`  THEN  Auto)

---

Home Index