---

Step * 1 2 of Lemma first-member-iff


1. [T] : Type
2. L : T List
3. P : T ⟶ 𝔹
4. x : T
5. i : ℕ||L||
6. x = L[i] ∈ T
7. ↑(P x)
8. ∀j:ℕi. (¬↑(P L[j]))
9. L = (firstn(i;L) @ [x / nth_tl(i + 1;L)]) ∈ (T List)
10. ↑(P x)
⊢ (∀y∈firstn(i;L).¬↑(P y))
BY
{ ((RWO "l_all_iff" 0 THEN Auto)
   THEN (RWO "member-firstn" (-1)⋅ THENA Auto)
   THEN ExRepD
   THEN (HypSubst (-1) 0 THENA Auto)
   THEN BackThruSomeHyp) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  P  :  T  {}\mrightarrow{}  \mBbbB{}
4.  x  :  T
5.  i  :  \mBbbN{}||L||
6.  x  =  L[i]
7.  \muparrow{}(P  x)
8.  \mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  L[j]))
9.  L  =  (firstn(i;L)  @  [x  /  nth\_tl(i  +  1;L)])
10.  \muparrow{}(P  x)
\mvdash{}  (\mforall{}y\mmember{}firstn(i;L).\mneg{}\muparrow{}(P  y))


By

---

Latex:
((RWO  "l\_all\_iff"  0  THEN  Auto)
  THEN  (RWO  "member-firstn"  (-1)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (HypSubst  (-1)  0  THENA  Auto)
  THEN  BackThruSomeHyp)

---

Home Index