---

Step * of Lemma permutation-nil-iff

∀[A:Type]. ∀L:A List. (permutation(A;[];L) ⇐⇒ L = [] ∈ (A List))
BY
{ Auto }

1
1. A : Type
2. L : A List
3. permutation(A;[];L)
⊢ L = [] ∈ (A List)

2
1. [A] : Type
2. L : A List
3. L = [] ∈ (A List)
⊢ permutation(A;[];L)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}L:A  List.  (permutation(A;[];L)  \mLeftarrow{}{}\mRightarrow{}  L  =  [])


By

---

Latex:
Auto

---

Home Index