---

Step * of Lemma l_exists_append

∀[T:Type]. ∀[P:T ⟶ ℙ].  ∀L1,L2:T List.  ((∃x∈L1 @ L2. P[x]) ⇐⇒ (∃x∈L1. P[x]) ∨ (∃x∈L2. P[x]))
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN RWO "l_exists_iff" 0
          THEN Auto
          THEN Try ((((RWO "member_append" (-1)) THENA Auto)
                     THEN ExRepD
                     THEN (ParallelOp (-2))
                     THEN AutoInstConcl []
                     THEN Auto))) }

1
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])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}L1,L2:T  List.    ((\mexists{}x\mmember{}L1  @  L2.  P[x])  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}x\mmember{}L1.  P[x])  \mvee{}  (\mexists{}x\mmember{}L2.  P[x]))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  RWO  "l\_exists\_iff"  0
                THEN  Auto
                THEN  Try  ((((RWO  "member\_append"  (-1))  THENA  Auto)
                                      THEN  ExRepD
                                      THEN  (ParallelOp  (-2))
                                      THEN  AutoInstConcl  []
                                      THEN  Auto)))

---

Home Index