---

Step * of Lemma Wadd_wf

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero:A ⟶ 𝔹]. ∀[w2,w1:W(A;a.B[a])].  ((w1 + w2) ∈ W(A;a.B[a]))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN WElim (-1)
   THEN RecUnfold `Wadd` 0
   THEN Unfold `Wsup` 0
   THEN Reduce 0
   THEN All (Fold `Wsup`)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[zero:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[w2,w1:W(A;a.B[a])].    ((w1  +  w2)  \mmember{}  W(A;a.B[a]))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  WElim  (-1)
  THEN  RecUnfold  `Wadd`  0
  THEN  Unfold  `Wsup`  0
  THEN  Reduce  0
  THEN  All  (Fold  `Wsup`)
  THEN  Auto)

---

Home Index