---

Step * of Lemma Wzero-unique

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero:A ⟶ 𝔹].
  ∀[z1,z2:W(A;a.B[a])].  z1 = z2 ∈ W(A;a.B[a]) supposing isZero(z1) ∧ isZero(z2) 
  supposing (∀a1,a2:A.  ((↑(zero a1)) ⇒ (↑(zero a2)) ⇒ (a1 = a2 ∈ A))) ∧ (∀a:A. ((¬B[a]) ⇒ (↑(zero a))))
BY
{ (Auto
   THEN RepeatFor 4 (MoveToConcl (-1))
   THEN RepeatFor 2 (UseWInductionLemma)
   THEN RepUR ``Wzero Wsup`` 0
   THEN Auto
   THEN Fold `Wsup` 0
   THEN EqCD
   THEN Auto
   THEN Ext
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[zero:A  {}\mrightarrow{}  \mBbbB{}].
    \mforall{}[z1,z2:W(A;a.B[a])].    z1  =  z2  supposing  isZero(z1)  \mwedge{}  isZero(z2) 
    supposing  (\mforall{}a1,a2:A.    ((\muparrow{}(zero  a1))  {}\mRightarrow{}  (\muparrow{}(zero  a2))  {}\mRightarrow{}  (a1  =  a2)))
    \mwedge{}  (\mforall{}a:A.  ((\mneg{}B[a])  {}\mRightarrow{}  (\muparrow{}(zero  a))))


By

---

Latex:
(Auto
  THEN  RepeatFor  4  (MoveToConcl  (-1))
  THEN  RepeatFor  2  (UseWInductionLemma)
  THEN  RepUR  ``Wzero  Wsup``  0
  THEN  Auto
  THEN  Fold  `Wsup`  0
  THEN  EqCD
  THEN  Auto
  THEN  Ext
  THEN  Auto)

---

Home Index