---

Step * of Lemma num-eq-constraints_wf

∀[p:IntConstraints]. (num-eq-constraints(p) ∈ ℕ)
BY
{ (Auto THEN D 1) }

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

2
1. y : Unit
⊢ num-eq-constraints(inr y ) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[p:IntConstraints].  (num-eq-constraints(p)  \mmember{}  \mBbbN{})


By

---

Latex:
(Auto  THEN  D  1)

---

Home Index