---

Step * 1 of Lemma num-eq-constraints_wf


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

---

Latex:

---

Latex:

1.  x  :  \mcup{}n:\mBbbN{}.(\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List  \mtimes{}  (\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List))
\mvdash{}  num-eq-constraints(inl  x)  \mmember{}  \mBbbN{}


By

---

Latex:
((D\_union  1  THEN  D  2)  THEN  ProveWfLemma)

---

Home Index