---

Step * of Lemma W-uwellfounded

∀[A:Type]. ∀[B:A ⟶ Type].  uWellFnd(W(A;a.B[a]);w1,w2.w1 <  w2)
BY
{ (UseWitness ⌜λF.fix(F)⌝⋅ THEN (BLemma_o W-uwellfounded_witness)) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    uWellFnd(W(A;a.B[a]);w1,w2.w1  <    w2)


By

---

Latex:
(UseWitness  \mkleeneopen{}\mlambda{}F.fix(F)\mkleeneclose{}\mcdot{}  THEN  (BLemma\_o  W-uwellfounded\_witness))

---

Home Index