Step
*
of Lemma
es-prior-interface_wf1
∀[Info,T:Type]. ∀[X:EClass(T)]. (prior(X) ∈ EClass(E(X)))
BY
{ ProveWfLemma }
1
1. Info : Type
2. T : Type
3. X : EClass(T)
⊢ local-pred-class(λes,e. e ∈b X) ∈ EClass(E(X))
Latex:
Latex:
\mforall{}[Info,T:Type]. \mforall{}[X:EClass(T)]. (prior(X) \mmember{} EClass(E(X)))
By
Latex:
ProveWfLemma
Home
Index