---

Step * 1 of Lemma reject_wf


1. A : Type
2. l : A List
3. n : ℤ
4. n < 1
⊢ l\[n] ∈ A List
BY
{ (RecUnfold `reject` 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  l  :  A  List
3.  n  :  \mBbbZ{}
4.  n  <  1
\mvdash{}  l\mbackslash{}[n]  \mmember{}  A  List


By

---

Latex:
(RecUnfold  `reject`  0  THEN  AutoSplit)

---

Home Index