---

Step * 2 1 of Lemma reject_wf


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
BY
{ (Decide ⌜n = 1 ∈ ℤ⌝⋅ THEN Auto THEN HypSubst' (-1) 0 THEN RecUnfold `reject` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  n  :  \mBbbZ{}
3.  \mneg{}(n  \mleq{}  0)
4.  0  <  n
5.  (\mneg{}n  -  1  <  1)  {}\mRightarrow{}  (\mforall{}l:A  List.  (l\mbackslash{}[n  -  1]  \mmember{}  A  List))
6.  \mneg{}n  <  1
7.  l  :  A  List
8.  ff  \mmember{}  \mBbbB{}
9.  a'  :  A
10.  as'  :  A  List
11.  A  List
\mvdash{}  as'\mbackslash{}[n  -  1]  \mmember{}  A  List


By

---

Latex:
(Decide  \mkleeneopen{}n  =  1\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  HypSubst'  (-1)  0  THEN  RecUnfold  `reject`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index