---

Step * of Lemma Wzero-leq

∀[A:Type]. ∀[B:A ⟶ Type].  ∀w:W(A;a.B[a]). (isZero(w) ⇐⇒ ∀w2:W(A;a.B[a]). (w ≤  w2))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN UseWInductionLemma THEN ReduceWcmp 0 THEN RepUR ``Wzero Wsup`` 0 THEN Auto) }

1
1. A : Type
2. B : A ⟶ Type
3. a : A@i
4. f : B[a] ⟶ W(A;a.B[a])@i
5. ∀b:B[a]. (isZero(f b) ⇐⇒ ∀w2:W(A;a.B[a]). ((f b) ≤  w2))@i
6. ∀w2:W(A;a.B[a]). ∀x:B[a].  ((f x) <  w2)@i
⊢ ¬B[a]

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    \mforall{}w:W(A;a.B[a]).  (isZero(w)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}w2:W(A;a.B[a]).  (w  \mleq{}    w2))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  UseWInductionLemma
  THEN  ReduceWcmp  0
  THEN  RepUR  ``Wzero  Wsup``  0
  THEN  Auto)

---

Home Index