---

Step * of Lemma until-class_local

∀[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[Y:EClass(C)].  (LocalClass(X) ⇒ LocalClass(Y) ⇒ LocalClass((X until Y)))
BY
{ (Auto THEN RenameVar `xpr' (-2) THEN RenameVar `ypr' (-1) THEN UseWitness ⌜until-class-program(xpr;ypr)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B)].  \mforall{}[Y:EClass(C)].
    (LocalClass(X)  {}\mRightarrow{}  LocalClass(Y)  {}\mRightarrow{}  LocalClass((X  until  Y)))


By

---

Latex:
(Auto
  THEN  RenameVar  `xpr'  (-2)
  THEN  RenameVar  `ypr'  (-1)
  THEN  UseWitness  \mkleeneopen{}until-class-program(xpr;ypr)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index