---

Step * of Lemma l_member_decomp

∀[T:Type]. ∀l:T List. ∀x:T.  ((x ∈ l) ⇐⇒ ∃l1,l2:T List. (l = (l1 @ [x] @ l2) ∈ (T List)))
BY
{ (((InductionOnList THEN RWW "cons_member" 0) THENM RWW "nil_member" 0) THEN Auto THEN ExRepD) }

1
1. T : Type
2. x : T
3. l1 : T List
4. l2 : T List
5. [] = (l1 @ [x] @ l2) ∈ (T List)
⊢ False

2
1. [T] : Type
2. u : T
3. v : T List
4. ∀x:T. ((x ∈ v) ⇐⇒ ∃l1,l2:T List. (v = (l1 @ [x] @ l2) ∈ (T List)))
5. x : T
6. (x = u ∈ T) ∨ (x ∈ v)
⊢ ∃l1,l2:T List. ([u / v] = (l1 @ [x] @ l2) ∈ (T List))

3
1. [T] : Type
2. u : T
3. v : T List
4. ∀x:T. ((x ∈ v) ⇐⇒ ∃l1,l2:T List. (v = (l1 @ [x] @ l2) ∈ (T List)))
5. x : T
6. l1 : T List
7. l2 : T List
8. [u / v] = (l1 @ [x] @ l2) ∈ (T List)
⊢ (x = u ∈ T) ∨ (x ∈ v)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}l:T  List.  \mforall{}x:T.    ((x  \mmember{}  l)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}l1,l2:T  List.  (l  =  (l1  @  [x]  @  l2)))


By

---

Latex:
(((InductionOnList  THEN  RWW  "cons\_member"  0)  THENM  RWW  "nil\_member"  0)  THEN  Auto  THEN  ExRepD)

---

Home Index