Step
*
2
of Lemma
l_exists_cons
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])
BY
{ TACTIC:(((D (-1)) THENL [(InstConcl [x]⋅ THEN Auto); (ParallelOp (-1))]) THEN ExRepD THEN SimpConcl) }
Latex:
Latex:
1. [T] : Type
2. [P] : T {}\mrightarrow{} \mBbbP{}
3. x : T
4. L : T List
5. P[x] \mvee{} (\mexists{}y:T. ((y \mmember{} L) \mwedge{} P[y]))
\mvdash{} \mexists{}y:T. (((y = x) \mvee{} (y \mmember{} L)) \mwedge{} P[y])
By
Latex:
TACTIC:(((D (-1)) THENL [(InstConcl [x]\mcdot{} THEN Auto); (ParallelOp (-1))]) THEN ExRepD THEN SimpConcl)
Home
Index