---

Step * 2 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])
9. (w1 + z) = w1 ∈ W(A;a.B[a])
⊢ (z + w1) = w1 ∈ W(A;a.B[a])
BY
{ (Thin (-1)
   THEN MoveToConcl (-1)
   THEN UseWInductionLemma
   THEN Auto
   THEN RecUnfold `Wadd` 0
   THEN Unfold `Wsup` 0
   THEN Reduce 0
   THEN Fold `Wsup` 0
   THEN AutoSplit) }

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)
⊢ z = Wsup(a;f) ∈ W(A;a.B[a])

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

---

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])
9.  (w1  +  z)  =  w1
\mvdash{}  (z  +  w1)  =  w1


By

---

Latex:
(Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  UseWInductionLemma
  THEN  Auto
  THEN  RecUnfold  `Wadd`  0
  THEN  Unfold  `Wsup`  0
  THEN  Reduce  0
  THEN  Fold  `Wsup`  0
  THEN  AutoSplit)

---

Home Index