---

Step * 1 of Lemma l_member-permutation


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

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index