---

Step * 2 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. 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])
BY
{ (EqCD THEN Auto) }

---

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


By

---

Latex:
(EqCD  THEN  Auto)

---

Home Index