---

Step * 1 of Lemma l_all_cons


1. [T] : Type
2. [P] : T ⟶ ℙ
3. x : T
4. L : T List
5. P[x]
6. ∀y:T. ((y ∈ L) ⇒ P[y])
7. y : T
8. (y ∈ [x / L])
⊢ P[y]
BY
{ ((RWO "cons_member" (-1) THENM D -1) THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  x  :  T
4.  L  :  T  List
5.  P[x]
6.  \mforall{}y:T.  ((y  \mmember{}  L)  {}\mRightarrow{}  P[y])
7.  y  :  T
8.  (y  \mmember{}  [x  /  L])
\mvdash{}  P[y]


By

---

Latex:
((RWO  "cons\_member"  (-1)  THENM  D  -1)  THEN  Auto)

---

Home Index