---

Step * of Lemma int-problem-dimension_wf

∀[p:IntConstraints]. (dim(p) ∈ ℕ)
BY
{ (Auto THEN D 1) }

1
1. x : ⋃n:ℕ.({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List × ({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List))
⊢ dim(inl x) ∈ ℕ

2
1. y : Unit
⊢ dim(inr y ) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[p:IntConstraints].  (dim(p)  \mmember{}  \mBbbN{})


By

---

Latex:
(Auto  THEN  D  1)

---

Home Index