---

Step * 2 of Lemma reject_wf


1. A : Type
2. l : A List
3. n : ℤ
4. ¬n < 1
⊢ l\[n] ∈ A List
BY
{ ((SubsumeHyp ⌜ℕ⌝ 3⋅ THENA Auto)
   THEN MoveToConcl 2
   THEN MoveToConcl (-1)
   THEN NatInd (-1)
   THEN RecUnfold `reject` 0
   THEN Reduce 0
   THEN Auto) }

1
1. A : Type
2. n : ℤ
3. ¬(n ≤ 0)
4. 0 < n
5. (¬n - 1 < 1) ⇒ (∀l:A List. (l\[n - 1] ∈ A List))
6. ¬n < 1
7. l : A List
8. ff ∈ 𝔹
9. a' : A
10. as' : A List
11. A List
⊢ as'\[n - 1] ∈ A List

---

Latex:

---

Latex:

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


By

---

Latex:
((SubsumeHyp  \mkleeneopen{}\mBbbN{}\mkleeneclose{}  3\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  2
  THEN  MoveToConcl  (-1)
  THEN  NatInd  (-1)
  THEN  RecUnfold  `reject`  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index