---

Step * 2 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. a : A
9. f : B[a] ⟶ W(A;a.B[a])
10. ∀b:B[a]. ((z + f b) = (f b) ∈ W(A;a.B[a]))
11. ↑(zero a)
⊢ z = Wsup(a;f) ∈ W(A;a.B[a])
BY
{ (UsingVars [`zero'] (BLemma `Wzero-unique`) THEN Auto) }

1
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. a : A
9. f : B[a] ⟶ W(A;a.B[a])
10. ∀b:B[a]. ((z + f b) = (f b) ∈ W(A;a.B[a]))
11. ↑(zero a)
12. isZero(z)
⊢ isZero(Wsup(a;f))

---

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.  a  :  A
9.  f  :  B[a]  {}\mrightarrow{}  W(A;a.B[a])
10.  \mforall{}b:B[a].  ((z  +  f  b)  =  (f  b))
11.  \muparrow{}(zero  a)
\mvdash{}  z  =  Wsup(a;f)


By

---

Latex:
(UsingVars  [`zero']  (BLemma  `Wzero-unique`)  THEN  Auto)

---

Home Index