---

Step * of Lemma bind-class_local

∀[Info,A,B:Type].
  ∀[X:EClass(A)]. ∀[Y:A ⟶ EClass(B)].  (LocalClass(X) ⇒ (∀a:A. LocalClass(Y[a])) ⇒ LocalClass(X >a> Y[a])) 
  supposing valueall-type(B)
BY
{ (Auto⋅
   THEN RenameVar `xpr' (-2)
   THEN Unfold `all` -1
   THEN RenameVar `ypr' (-1)
   THEN UseWitness ⌜xpr >>= ypr⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].
    \mforall{}[X:EClass(A)].  \mforall{}[Y:A  {}\mrightarrow{}  EClass(B)].
        (LocalClass(X)  {}\mRightarrow{}  (\mforall{}a:A.  LocalClass(Y[a]))  {}\mRightarrow{}  LocalClass(X  >a>  Y[a])) 
    supposing  valueall-type(B)


By

---

Latex:
(Auto\mcdot{}
  THEN  RenameVar  `xpr'  (-2)
  THEN  Unfold  `all`  -1
  THEN  RenameVar  `ypr'  (-1)
  THEN  UseWitness  \mkleeneopen{}xpr  >>=  ypr\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index