Step
*
of Lemma
data_wf
∀[T:Id ─→ Type]. (data(T) ∈ Type)
BY
{ ProveWfLemma }
Latex:
\mforall{}[T:Id  {}\mrightarrow{}  Type].  (data(T)  \mmember{}  Type)
By
ProveWfLemma
Home
Index