---

Step * of Lemma permutation-contains

∀[A:Type]. ∀L1,L2:A List.  (permutation(A;L1;L2) ⇒ L2 ⊆ L1)
BY
{ (Auto
   THEN (FLemma `permutation-length` [-1] THENA Auto)
   THEN D (-2)
   THEN RepUR ``l_contains l_all`` 0
   THEN Auto
   THEN ExRepD
   THEN StrongHypSubst (-3) 0
   THEN Auto
   THEN RWW "permute_list_select" 0
   THEN Auto
   THEN HypSubst' (-1) 0
   THEN RWO "permute_list_length" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (FLemma  `permutation-length`  [-1]  THENA  Auto)
  THEN  D  (-2)
  THEN  RepUR  ``l\_contains  l\_all``  0
  THEN  Auto
  THEN  ExRepD
  THEN  StrongHypSubst  (-3)  0
  THEN  Auto
  THEN  RWW  "permute\_list\_select"  0
  THEN  Auto
  THEN  HypSubst'  (-1)  0
  THEN  RWO  "permute\_list\_length"  0
  THEN  Auto)

---

Home Index