---

Step * of Lemma altWind-induction

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[P:altW(A;a.B[a]) ⟶ ℙ].
  ((∀w:altW(A;a.B[a]). ((∀b:coW-dom(a.B[a];w). P[altW-item(w;b)]) ⇒ P[w])) ⇒ (∀w:altW(A;a.B[a]). P[w]))
BY
{ (Auto THEN RenameVar `h' (-2) THEN UseWitness ⌜altWind(h;w)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[P:altW(A;a.B[a])  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}w:altW(A;a.B[a]).  ((\mforall{}b:coW-dom(a.B[a];w).  P[altW-item(w;b)])  {}\mRightarrow{}  P[w]))
    {}\mRightarrow{}  (\mforall{}w:altW(A;a.B[a]).  P[w]))


By

---

Latex:
(Auto  THEN  RenameVar  `h'  (-2)  THEN  UseWitness  \mkleeneopen{}altWind(h;w)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index