---

Step * of Lemma permutation-equiv

∀[A:Type]. EquivRel(A List)(permutation(A;_1;_2))
BY
{ (Auto
   THEN RepeatFor 2 (D 0)
   THEN Auto
   THEN Try ((BLemma `permutation_weakening` THEN Auto))
   THEN D 0
   THEN Auto
   THEN Try ((FLemma `permutation_transitivity` [5;6] THEN Auto))
   THEN Try ((BLemma `permutation_inversion` THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  EquivRel(A  List)(permutation(A;$_{1}$;$_{2}$))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  0)
  THEN  Auto
  THEN  Try  ((BLemma  `permutation\_weakening`  THEN  Auto))
  THEN  D  0
  THEN  Auto
  THEN  Try  ((FLemma  `permutation\_transitivity`  [5;6]  THEN  Auto))
  THEN  Try  ((BLemma  `permutation\_inversion`  THEN  Auto)))

---

Home Index