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