---

Step * of Lemma permutation-map

∀[A:Type]. ∀L1,L2:A List.  (permutation(A;L1;L2) ⇒ (∀[B:Type]. ∀f:A ⟶ B. permutation(B;map(f;L1);map(f;L2))))
BY
{ (Auto
   THEN RepeatFor 3 (ParallelOp -3)
   THEN Try (((HypSubst (-3) 0 THENM BLemma `list_extensionality`) THEN Auto))
   THEN RWW "length-map permute_list_length map_select permute_list_select" 0
   THEN Auto
   THEN (All (RWW "length-map permute_list_length") THEN Auto THEN Auto')⋅) }

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}L1,L2:A  List.
        (permutation(A;L1;L2)  {}\mRightarrow{}  (\mforall{}[B:Type].  \mforall{}f:A  {}\mrightarrow{}  B.  permutation(B;map(f;L1);map(f;L2))))


By

---

Latex:
(Auto
  THEN  RepeatFor  3  (ParallelOp  -3)
  THEN  Try  (((HypSubst  (-3)  0  THENM  BLemma  `list\_extensionality`)  THEN  Auto))
  THEN  RWW  "length-map  permute\_list\_length  map\_select  permute\_list\_select"  0
  THEN  Auto
  THEN  (All  (RWW  "length-map  permute\_list\_length")  THEN  Auto  THEN  Auto')\mcdot{})

---

Home Index