---

Step * of Lemma implies_l_member_append

∀T:Type. ∀l1,l2:T List. ∀v:T.  (((v ∈ l1) ∨ (v ∈ l2)) ⇒ (v ∈ l1 @ l2))
BY
{ ((UnivCD THENA Auto) THEN All(RepUR ``l_member``) THEN DProdsAndUnions) }

1
1. T : Type
2. l1 : T List
3. l2 : T List
4. v : T
5. i : ℕ
6. i < ||l1||
7. v = l1[i] ∈ T
⊢ ∃i:ℕ. (i < ||l1 @ l2|| c∧ (v = l1 @ l2[i] ∈ T))

2
1. T : Type
2. l1 : T List
3. l2 : T List
4. v : T
5. i : ℕ
6. i < ||l2||
7. v = l2[i] ∈ T
⊢ ∃i:ℕ. (i < ||l1 @ l2|| c∧ (v = l1 @ l2[i] ∈ T))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}l1,l2:T  List.  \mforall{}v:T.    (((v  \mmember{}  l1)  \mvee{}  (v  \mmember{}  l2))  {}\mRightarrow{}  (v  \mmember{}  l1  @  l2))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  All(RepUR  ``l\_member``)  THEN  DProdsAndUnions)

---

Home Index