---

Step * 1 of Lemma l_exists_append


1. [T] : Type
2. [P] : T ⟶ ℙ
3. L1 : T List
4. L2 : T List
5. (∃x:T. ((x ∈ L1) ∧ P[x])) ∨ (∃x:T. ((x ∈ L2) ∧ P[x]))
⊢ ∃x:T. ((x ∈ L1 @ L2) ∧ P[x])
BY
{ (((D (-1) THEN ParallelOp (-1)) THEN RWO "member_append" 0) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  L1  :  T  List
4.  L2  :  T  List
5.  (\mexists{}x:T.  ((x  \mmember{}  L1)  \mwedge{}  P[x]))  \mvee{}  (\mexists{}x:T.  ((x  \mmember{}  L2)  \mwedge{}  P[x]))
\mvdash{}  \mexists{}x:T.  ((x  \mmember{}  L1  @  L2)  \mwedge{}  P[x])


By

---

Latex:
(((D  (-1)  THEN  ParallelOp  (-1))  THEN  RWO  "member\_append"  0)  THEN  Auto)\mcdot{}

---

Home Index