Step
*
of Lemma
es-le-interface_wf
∀[Info,A:Type]. ∀[X:EClass(A)]. (le(X) ∈ EClass(E(X)))
BY
{ (ProveWfLemma
THEN SubsumeC ⌈EClass({e:E| ↑((λes,e. e ∈b X) es e)} )⌉⋅
THEN Auto
THEN Reduce 0
THEN Fold `es-E-interface` 0
THEN Auto) }
Latex:
Latex:
\mforall{}[Info,A:Type]. \mforall{}[X:EClass(A)]. (le(X) \mmember{} EClass(E(X)))
By
Latex:
(ProveWfLemma
THEN SubsumeC \mkleeneopen{}EClass(\{e:E| \muparrow{}((\mlambda{}es,e. e \mmember{}\msubb{} X) es e)\} )\mkleeneclose{}\mcdot{}
THEN Auto
THEN Reduce 0
THEN Fold `es-E-interface` 0
THEN Auto)
Home
Index