---

Step * of Lemma permutation-cons

∀[A:Type]
  ∀x:A. ∀L1,L2:A List.
    (permutation(A;[x / L1];L2) ⇐⇒ ∃as,bs:A List. ((L2 = (as @ [x / bs]) ∈ (A List)) ∧ permutation(A;L1;as @ bs)))
BY
{ (Auto THEN ExRepD) }

1
1. [A] : Type
2. x : A
3. L1 : A List
4. L2 : A List
5. permutation(A;[x / L1];L2)
⊢ ∃as,bs:A List. ((L2 = (as @ [x / bs]) ∈ (A List)) ∧ permutation(A;L1;as @ bs))

2
1. [A] : Type
2. x : A
3. L1 : A List
4. L2 : A List
5. as : A List
6. bs : A List
7. L2 = (as @ [x / bs]) ∈ (A List)
8. permutation(A;L1;as @ bs)
⊢ permutation(A;[x / L1];L2)

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}x:A.  \mforall{}L1,L2:A  List.
        (permutation(A;[x  /  L1];L2)
        \mLeftarrow{}{}\mRightarrow{}  \mexists{}as,bs:A  List.  ((L2  =  (as  @  [x  /  bs]))  \mwedge{}  permutation(A;L1;as  @  bs)))


By

---

Latex:
(Auto  THEN  ExRepD)

---

Home Index