---

Step * of Lemma permutation-cons2

∀[A:Type]. ∀x:A. ∀L1,L2:A List.  (permutation(A;L1;L2) ⇒ permutation(A;[x / L1];[x / L2]))
BY
{ Auto }

1
1. [A] : Type
2. x : A@i
3. L1 : A List@i
4. L2 : A List@i
5. permutation(A;L1;L2)@i
⊢ permutation(A;[x / L1];[x / L2])

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}x:A.  \mforall{}L1,L2:A  List.    (permutation(A;L1;L2)  {}\mRightarrow{}  permutation(A;[x  /  L1];[x  /  L2]))


By

---

Latex:
Auto

---

Home Index