---

Step * of Lemma member-permutation

∀[A:Type]. ∀as,bs:A List.  (permutation(A;as;bs) ⇒ {∀a:A. ((a ∈ as) ⇐⇒ (a ∈ bs))})
BY
{ ((Auto THEN (Assert permutation(A;bs;as) BY (RelRST THEN Auto)))
   THEN RepeatFor 2 ((FLemma `permutation-contains` [-2] THENA Auto))
   ) }

1
1. [A] : Type
2. as : A List@i
3. bs : A List@i
4. permutation(A;as;bs)@i
5. permutation(A;bs;as)
6. bs ⊆ as
7. as ⊆ bs
⊢ {∀a:A. ((a ∈ as) ⇐⇒ (a ∈ bs))}

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}as,bs:A  List.    (permutation(A;as;bs)  {}\mRightarrow{}  \{\mforall{}a:A.  ((a  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  bs))\})


By

---

Latex:
((Auto  THEN  (Assert  permutation(A;bs;as)  BY  (RelRST  THEN  Auto)))
  THEN  RepeatFor  2  ((FLemma  `permutation-contains`  [-2]  THENA  Auto))
  )

---

Home Index