---

Step * of Lemma Wadd-assoc

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero:A ⟶ 𝔹]. ∀[w3,w2,w1:W(A;a.B[a])].  ((w1 + (w2 + w3)) = ((w1 + w2) + w3) ∈ W(A;a.B[a]))
BY
{ (Auto
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN UseWInductionLemma
   THEN Auto
   THEN RW (AddrC [3] RecUnfoldTopAbC) 0
   THEN RW (AddrC [2;3] RecUnfoldTopAbC) 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
5. ¬↑(zero a)
6. f : B[a] ⟶ W(A;a.B[a])
7. ∀b:B[a]. ∀w2,w1:W(A;a.B[a]).  ((w1 + (w2 + f b)) = ((w1 + w2) + f b) ∈ W(A;a.B[a]))
8. w2 : W(A;a.B[a])
9. w1 : W(A;a.B[a])
⊢ (w1 + Wsup(a;λx.(w2 + f x))) = Wsup(a;λx.((w1 + w2) + f x)) ∈ W(A;a.B[a])

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  UseWInductionLemma
  THEN  Auto
  THEN  RW  (AddrC  [3]  RecUnfoldTopAbC)  0
  THEN  RW  (AddrC  [2;3]  RecUnfoldTopAbC)  0
  THEN  Unfold  `Wsup`  0
  THEN  Reduce  0
  THEN  Fold  `Wsup`  0
  THEN  AutoSplit)

---

Home Index