Step
*
of Lemma
eclass3_local
∀[Info,B,C:Type]. ∀[X:EClass(B ─→ C)]. ∀[Y:EClass(B)].
LocalClass(X)
⇒ LocalClass(Y)
⇒ LocalClass(eclass3(X;Y)) supposing valueall-type(C)
BY
{ (Auto THEN RenameVar `Xpr' (-2) THEN RenameVar `Ypr' (-1) THEN UseWitness ⌈eclass3-program(Xpr;Ypr)⌉⋅ THEN Auto) }
Latex:
Latex:
\mforall{}[Info,B,C:Type]. \mforall{}[X:EClass(B {}\mrightarrow{} C)]. \mforall{}[Y:EClass(B)].
LocalClass(X) {}\mRightarrow{} LocalClass(Y) {}\mRightarrow{} LocalClass(eclass3(X;Y)) supposing valueall-type(C)
By
Latex:
(Auto
THEN RenameVar `Xpr' (-2)
THEN RenameVar `Ypr' (-1)
THEN UseWitness \mkleeneopen{}eclass3-program(Xpr;Ypr)\mkleeneclose{}\mcdot{}
THEN Auto)
Home
Index