Step
*
of Lemma
es-interval_wf2
∀[es:EO]. ∀[e,e':E]. ([e, e'] ∈ {ev:E| loc(ev) = loc(e') ∈ Id} List)
BY
{ (Auto THEN BLemma `list-set-type2` THEN Auto) }
1
1. es : EO
2. e : E
3. e' : E
⊢ (∀ev∈[e, e'].loc(ev) = loc(e') ∈ Id)
Latex:
\mforall{}[es:EO]. \mforall{}[e,e':E]. ([e, e'] \mmember{} \{ev:E| loc(ev) = loc(e')\} List)
By
(Auto THEN BLemma `list-set-type2` THEN Auto)
Home
Index