---

Step * of Lemma ctt-arity_wf

No Annotations
∀[x:CttOp]. (ctt-arity(x) ∈ (ℕ × ℕ) List)
BY
{ (Intro THEN Unhide THEN D -1 THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x:CttOp].  (ctt-arity(x)  \mmember{}  (\mBbbN{}  \mtimes{}  \mBbbN{})  List)


By

---

Latex:
(Intro  THEN  Unhide  THEN  D  -1  THEN  ProveWfLemma)

---

Home Index