---

Step * of Lemma Wmul_wf

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero,succ:A ⟶ 𝔹]. ∀[w2,w1:W(A;a.B[a])].
  (w1 * w2) ∈ W(A;a.B[a]) supposing ∀a:A. ((↑(succ a)) ⇒ (Unit ⊆r B[a]))
BY
{ (RepeatFor 5 ((D 0 THENA Auto))
   THEN WElim (-1)
   THEN RecUnfold `Wmul` 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,succ:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[w2,w1:W(A;a.B[a])].
    (w1  *  w2)  \mmember{}  W(A;a.B[a])  supposing  \mforall{}a:A.  ((\muparrow{}(succ  a))  {}\mRightarrow{}  (Unit  \msubseteq{}r  B[a]))


By

---

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

---

Home Index