---

Step * of Lemma cons_functionality_wrt_permutation

∀[A:Type]. ∀L1,L2:A List. ∀x:A.  (permutation(A;L1;L2) ⇒ permutation(A;[x / L1];[x / L2]))
BY
{ (Auto
   THEN Subst' [x / L1] ~ [x] @ L1 0
   THEN Try (Complete ((Reduce 0 THEN Auto)))
   THEN Subst' [x / L2] ~ [x] @ L2 0
   THEN Try (Complete ((Reduce 0 THEN Auto)))) }

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Subst'  [x  /  L1]  \msim{}  [x]  @  L1  0
  THEN  Try  (Complete  ((Reduce  0  THEN  Auto)))
  THEN  Subst'  [x  /  L2]  \msim{}  [x]  @  L2  0
  THEN  Try  (Complete  ((Reduce  0  THEN  Auto))))

---

Home Index