---

Step * of Lemma test-exact-eq-constraint_wf

∀[L:ℤ List]. (test-exact-eq-constraint(L) ∈ ∃i:ℕ||L|| [(|L[i]| = 1 ∈ ℤ)]?)
BY
{ (Unfolds ``sq_exists test-exact-eq-constraint`` 0 THEN InductionOnList THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  (test-exact-eq-constraint(L)  \mmember{}  \mexists{}i:\mBbbN{}||L||  [(|L[i]|  =  1)]?)


By

---

Latex:
(Unfolds  ``sq\_exists  test-exact-eq-constraint``  0  THEN  InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index