---

Step * of Lemma l_exists_cons

∀[T:Type]. ∀[P:T ⟶ ℙ].  ∀x:T. ∀L:T List.  ((∃y∈[x / L]. P[y]) ⇐⇒ P[x] ∨ (∃y∈L. P[y]))
BY
{ ((UnivCD THENA Auto) THEN (((RWO "l_exists_iff" 0 THENA Auto) THEN RWO "cons_member" 0) THEN Auto) THEN ExRepD) }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. x : T
4. L : T List
5. y : T
6. (y = x ∈ T) ∨ (y ∈ L)
7. P[y]
⊢ P[x] ∨ (∃y:T. ((y ∈ L) ∧ P[y]))

2
1. [T] : Type
2. [P] : T ⟶ ℙ
3. x : T
4. L : T List
5. P[x] ∨ (∃y:T. ((y ∈ L) ∧ P[y]))
⊢ ∃y:T. (((y = x ∈ T) ∨ (y ∈ L)) ∧ P[y])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x:T.  \mforall{}L:T  List.    ((\mexists{}y\mmember{}[x  /  L].  P[y])  \mLeftarrow{}{}\mRightarrow{}  P[x]  \mvee{}  (\mexists{}y\mmember{}L.  P[y]))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (((RWO  "l\_exists\_iff"  0  THENA  Auto)  THEN  RWO  "cons\_member"  0)  THEN  Auto)
  THEN  ExRepD)

---

Home Index