---

Step * of Lemma l_member-permutation

∀[T:Type]. ∀L:T List. ∀x:T.  ((x ∈ L) ⇒ (∃L':T List. permutation(T;L;[x / L'])))
BY
{ InductionOnList }

1
1. [T] : Type
⊢ ∀x:T. ((x ∈ []) ⇒ (∃L':T List. permutation(T;[];[x / L'])))

2
1. [T] : Type
2. u : T@i
3. v : T List@i
4. ∀x:T. ((x ∈ v) ⇒ (∃L':T List. permutation(T;v;[x / L'])))@i
⊢ ∀x:T. ((x ∈ [u / v]) ⇒ (∃L':T List. permutation(T;[u / v];[x / L'])))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}x:T.    ((x  \mmember{}  L)  {}\mRightarrow{}  (\mexists{}L':T  List.  permutation(T;L;[x  /  L'])))


By

---

Latex:
InductionOnList

---

Home Index