---

Step * 1 of Lemma Wadd-Wzero


1. A : Type
2. B : A ⟶ Type
3. zero : A ⟶ 𝔹
4. ∀a:A. (↑(zero a) ⇐⇒ ¬B[a])
5. ∀a1,a2:A.  ((↑(zero a1)) ⇒ (↑(zero a2)) ⇒ (a1 = a2 ∈ A))
6. z : W(A;a.B[a])
7. isZero(z)
8. w1 : W(A;a.B[a])
⊢ (w1 + z) = w1 ∈ W(A;a.B[a])
BY
{ (RepeatFor 3 (MoveToConcl (-1))
   THEN UseWInductionLemma
   THEN RepUR ``Wzero Wsup`` 0
   THEN RecUnfold `Wadd` 0
   THEN Reduce 0
   THEN Auto
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  zero  :  A  {}\mrightarrow{}  \mBbbB{}
4.  \mforall{}a:A.  (\muparrow{}(zero  a)  \mLeftarrow{}{}\mRightarrow{}  \mneg{}B[a])
5.  \mforall{}a1,a2:A.    ((\muparrow{}(zero  a1))  {}\mRightarrow{}  (\muparrow{}(zero  a2))  {}\mRightarrow{}  (a1  =  a2))
6.  z  :  W(A;a.B[a])
7.  isZero(z)
8.  w1  :  W(A;a.B[a])
\mvdash{}  (w1  +  z)  =  w1


By

---

Latex:
(RepeatFor  3  (MoveToConcl  (-1))
  THEN  UseWInductionLemma
  THEN  RepUR  ``Wzero  Wsup``  0
  THEN  RecUnfold  `Wadd`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  AutoSplit)

---

Home Index