---

Step * 1 2 1 of Lemma first-member-cons


1. T : Type
2. P : T ⟶ 𝔹
3. x : T
4. u : T
5. ¬↑(P u)
6. L : T List
7. i : ℕ||[u / L]||
8. x = L[i - 1] ∈ T
9. ↑(P x)
10. ∀j:ℕi. (¬↑(P [u / L][j]))
11. ¬(i = 0 ∈ ℤ)
12. ¬False
13. x = L[i - 1] ∈ T
14. ↑(P x)
15. j : ℕi - 1
⊢ ¬↑(P L[j])
BY
{ xxxOnMaybeHyp 10 (\h. ((InstHyp [⌜j + 1⌝] h⋅ THENA Auto) THEN RWO "select-cons-tl" (-1) THEN Auto))xxx }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  x  :  T
4.  u  :  T
5.  \mneg{}\muparrow{}(P  u)
6.  L  :  T  List
7.  i  :  \mBbbN{}||[u  /  L]||
8.  x  =  L[i  -  1]
9.  \muparrow{}(P  x)
10.  \mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  [u  /  L][j]))
11.  \mneg{}(i  =  0)
12.  \mneg{}False
13.  x  =  L[i  -  1]
14.  \muparrow{}(P  x)
15.  j  :  \mBbbN{}i  -  1
\mvdash{}  \mneg{}\muparrow{}(P  L[j])


By

---

Latex:
xxxOnMaybeHyp  10  (\mbackslash{}h.
((InstHyp  [\mkleeneopen{}j  +  1\mkleeneclose{}]  h\mcdot{}  THENA  Auto)  THEN  RWO  "select-cons-tl"  (-1)  THEN  Auto))xxx

---

Home Index