Definition equiv_lst l m := ∀ (x : Atom), In x l ↔ In x m.
Notation "l ≈ m" := (equiv_lst l m)(at level 60).

Global Instance equiv_lst_refl : Reflexive equiv_lst.
Global Instance equiv_lst_sym : Symmetric equiv_lst.
Global Instance equiv_lst_trans : Transitive equiv_lst.
Global Instance equiv_lst_Equiv : Equivalence equiv_lst.

Definition incl_lst l m := ∀ (x : Atom), In x l → In x m.

Global Instance pre_incl_lst : PreOrder incl_lst.

Global Instance anti_incl_lst : PartialOrder equiv_lst incl_lst.

Global Instance antisym_incl_lst : Antisymmetric (list Atom)
                                                 equiv_lst incl_lst.
Notation "l ⊆ m" := (incl_lst l m)(at level 60).
Global Instance In_equiv a :
  Proper (equiv_lst ==> Basics.impl) (In a).
Global Instance In_incl a :
  Proper (incl_lst ==> Basics.impl) (In a).

Definition incl_lst_b l m :=
  forallb (fun x ⇒ inb x m) l.
Lemma incl_lst_b_spec l m : reflect (l ⊆ m) (incl_lst_b l m).

Definition equiv_lst_b l m := (incl_lst_b l m && incl_lst_b m l)%bool.
Lemma equiv_lst_b_spec l m : reflect (l ≈ m) (equiv_lst_b l m).

Lemma cons_comm a b l m :
  l ≈ m → (a :: b :: l) ≈ (b :: a :: m).
Lemma purge_cong l1 l2 m1 m2 :
  l1 ≈ l2 → m1 ≈ m2 → l1 -- m1 ≈ l2 -- m2.
Lemma app_cong l1 l2 m1 m2 :
  l1 ≈ l2 → m1 ≈ m2 → (l1 ++ m1) ≈ (l2 ++ m2).
Lemma undup_equiv_lst l : 〈l〉 ≈ l.
Lemma inter_cong l1 l2 m1 m2 :
  l1 ≈ l2 → m1 ≈ m2 → l1 ∩ m1 ≈ l2 ∩ m2.

Lemma cons_cong a l m : l≈m → (a::l) ≈ (a::m).

Lemma rm_cong a l m : l≈m → (rm a l) ≈ (rm a m).
Lemma mact_cong p l m : p ⧓ l ≈ p ⧓ m ↔ l ≈ m.

Global Instance rm_equiv a : Proper (equiv_lst ==> equiv_lst) (rm a).
Global Instance cons_equiv a :
  Proper (equiv_lst ==> equiv_lst) (cons a).
Global Instance purge_equiv :
  Proper (equiv_lst ==> equiv_lst ==> equiv_lst) purge.
Global Instance purge_eq :
  Proper (Logic.eq ==> equiv_lst ==> Logic.eq) purge.
Global Instance inter_equiv :
  Proper (equiv_lst ==> equiv_lst ==> equiv_lst) inter.
Global Instance rm_incl a : Proper (incl_lst ==> incl_lst) (rm a).
Global Instance cons_incl a : Proper (incl_lst ==> incl_lst) (cons a).
Global Instance purge_incl :
  Proper (incl_lst ==> equiv_lst ==> incl_lst) purge.
Global Instance inter_incl :
  Proper (incl_lst ==> incl_lst ==> incl_lst) inter.
Global Instance mact_equiv p :
  Proper (equiv_lst ==> equiv_lst) (mact p).
Global Instance mact_incl p : Proper (incl_lst ==> incl_lst) (mact p).
Global Instance undup_equiv : Proper (equiv_lst ==> equiv_lst) undup.
Global Instance app_equiv :
  Proper (equiv_lst ==> equiv_lst ==> equiv_lst) (@app Atom).
Global Instance app_incl :
  Proper (incl_lst ==> incl_lst ==> incl_lst) (@app Atom).

Lemma cons_rm_eq a l m : ¬ In a m → l ≈ (a::m) → In a l ∧ rm a l ≈ m.

Lemma rm_cons_eq a l m : In a l → rm a l ≈ m → ¬ In a m ∧ l ≈ (a::m).

Lemma rm_cons_eq' a l : In a l → l ≈ (a :: rm a l).
Lemma cons_rm_eq' a m : ¬ In a m → rm a (a::m) ≈ m.
Lemma purge_l_m_nil l m : l ⊆ m → l -- m = [].
Lemma app_l_l l : (l++l) ≈ l.

Lemma map_act_inv_eq p l m : p ⧓ l ≈ m ↔ l ≈ p⋆ ⧓ m.

Lemma map1 p l m : l ⊆ (p⋆) ⧓ m ↔ p ⧓ l ⊆ m.

Lemma map2 p l m : l ⊆ p ⧓ m ↔ (p⋆) ⧓ l ⊆ m.
Lemma app_com l m : (l ++ m) ≈ (m ++ l).

Fixpoint elements (p : perm) :=
  match p with
  | [] ⇒ []
  | (a,b)::p ⇒ a::b::(elements p)
  end.
Lemma elements_inv_act x p :
  ¬ In x (elements p) → p⋈x = x.
Lemma elements_inv_mact x p :
  (∀ y, In y x → ¬ In y (elements p)) → p⧓x = x.
Lemma elements_app : ∀ p q,
    elements (p++q) ≈ (elements p ++ elements q).
Lemma elements_inv_eq :∀ q, elements q ≈ elements (q⋆).

Lemma elements_act_in_equiv : ∀ q a,
    In a (elements q) ↔ In (q⋈a) (elements q).

Lemma elements_in_mact : ∀ l y q,
    In y (q ⧓ l) → In y l ∨ In y (elements q).

Lemma mact_elements_equiv_perm p q :
  p ≌ q ↔
  (∀ x, In x (elements p ++ elements q) → p⋈x = q⋈x).

Definition bequiv_perm p q :=
  forallb (fun x ⇒ beq_atom (p⋈x) (q⋈x)) (elements p ++ elements q).
Lemma bequiv_perm_spec p q : reflect (p ≌ q) (bequiv_perm p q).