Step
*
of Lemma
skip-first-class_wf
∀[Info,A:Type]. ∀[X:EClass(A)]. (Skip(X) ∈ EClass(A))
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[Info,A:Type]. \mforall{}[X:EClass(A)]. (Skip(X) \mmember{} EClass(A))
By
Latex:
ProveWfLemma
Home
Index