---

Step * of Lemma Wmul-Wzero

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero,succ:A ⟶ 𝔹].
  ∀[z:W(A;a.B[a])]. ∀[w1:W(A;a.B[a])]. ((w1 * z) = z ∈ W(A;a.B[a])) supposing isZero(z) 
  supposing ∀a:A. ((↑(succ a)) ⇒ (Unit ⊆r B[a]))
BY
{ (Auto
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN UseWInductionLemma
   THEN RepUR ``Wzero Wsup`` 0
   THEN RecUnfold `Wmul` 0
   THEN Reduce 0
   THEN Auto
   THEN AutoSplit
   THEN Try ((Fold `Wsup` 0 THEN EqCD THEN Auto THEN Ext THEN Auto)⋅)
   THEN (D (-3) THEN UseWitness ⌜⋅⌝ THEN DoSubsume⋅ THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[zero,succ:A  {}\mrightarrow{}  \mBbbB{}].
    \mforall{}[z:W(A;a.B[a])].  \mforall{}[w1:W(A;a.B[a])].  ((w1  *  z)  =  z)  supposing  isZero(z) 
    supposing  \mforall{}a:A.  ((\muparrow{}(succ  a))  {}\mRightarrow{}  (Unit  \msubseteq{}r  B[a]))


By

---

Latex:
(Auto
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  UseWInductionLemma
  THEN  RepUR  ``Wzero  Wsup``  0
  THEN  RecUnfold  `Wmul`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  AutoSplit
  THEN  Try  ((Fold  `Wsup`  0  THEN  EqCD  THEN  Auto  THEN  Ext  THEN  Auto)\mcdot{})
  THEN  (D  (-3)  THEN  UseWitness  \mkleeneopen{}\mcdot{}\mkleeneclose{}  THEN  DoSubsume\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index