Step
*
of Lemma
es-is-le-interface
∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E. (↑e ∈b le(X)
⇐⇒ ∃e':E. (e' ≤loc e ∧ (↑e' ∈b X)))
BY
{ ((UnivCD THENA Auto)
THEN ((InstLemma `es-local-le-pred-property` [⌈Info⌉;⌈λes,e. e ∈b X⌉;⌈es⌉;⌈e⌉])⋅ THENA Auto)
THEN (Reduce (-1))
THEN (Fold `es-le-interface` (-1))
THEN D -1
THEN Trivial) }
Latex:
Latex:
\mforall{}[Info:Type]
\mforall{}es:EO+(Info). \mforall{}X:EClass(Top). \mforall{}e:E. (\muparrow{}e \mmember{}\msubb{} le(X) \mLeftarrow{}{}\mRightarrow{} \mexists{}e':E. (e' \mleq{}loc e \mwedge{} (\muparrow{}e' \mmember{}\msubb{} X)))
By
Latex:
((UnivCD THENA Auto)
THEN ((InstLemma `es-local-le-pred-property` [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}\mlambda{}es,e. e \mmember{}\msubb{} X\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}])\mcdot{} THENA Auto)
THEN (Reduce (-1))
THEN (Fold `es-le-interface` (-1))
THEN D -1
THEN Trivial)
Home
Index