Step
*
of Lemma
ctt-kind_wf
No Annotations
∀[t:term(CttOp)]. (ctt-kind(t) ∈ ℕ)
BY
{ ProveWfLemma }
Latex:
Latex:
No  Annotations
\mforall{}[t:term(CttOp)].  (ctt-kind(t)  \mmember{}  \mBbbN{})
By
Latex:
ProveWfLemma
Home
Index