Require Import Infrastructure.
Require Import Env.

Definition transp_atom (x y z: atom) : atom :=
  if (x == z)
  then y
  else
    if (y == z)
    then x
    else z.

Lemma transp_atom_swap x y z:
  transp_atom x y z = transp_atom y x z.
Proof.
  unfold transp_atom.
  destruct (x == z); destruct (y == z); congruence.
Qed.

Lemma transp_atom_thisR y z:
  transp_atom y z z = y.
Proof.
  unfold transp_atom.
  destruct (z == z); try contradiction.
  destruct (y == z); congruence.
Qed.

Lemma transp_atom_thisL x y:
  transp_atom x y x = y.
Proof.
  rewrite transp_atom_swap. apply transp_atom_thisR.
Qed.

Lemma transp_atom_other x y z:
  x ≠ z →
  y ≠ z →
  transp_atom x y z = z.
Proof.
  intros Hx Hy.
  unfold transp_atom.
  destruct (x == z); destruct (y == z); congruence.
Qed.

Lemma transp_atom_refl x z:
  transp_atom x x z = z.
Proof.
  unfold transp_atom. destruct (x == z); congruence.
Qed.

Lemma transp_atom_trans x1 x2 x3 z:
  x1 ≠ z →
  x2 ≠ z →
  transp_atom x1 x2 (transp_atom x2 x3 z) = transp_atom x1 x3 z.
Proof.
  intros H1 H2.
  destruct (x3 == z); subst.
  - repeat rewrite transp_atom_thisR. reflexivity.
  - destruct (x2 == z); subst; [contradiction |].
    rewrite (transp_atom_other x2 x3); auto.
    destruct (x1 == z); subst; [contradiction |].
    repeat rewrite transp_atom_other; auto.
Qed.

Lemma transp_atom_involution x y z:
  transp_atom x y (transp_atom x y z) = z.
Proof.
  rewrite (transp_atom_swap x y z).
  destruct (y == z); [| destruct (x == z)]; subst; auto.
  - rewrite transp_atom_thisL. rewrite transp_atom_thisL. reflexivity.
  - rewrite transp_atom_thisR. rewrite transp_atom_thisR. reflexivity.
  - rewrite transp_atom_trans; auto. rewrite transp_atom_refl. reflexivity.
Qed.

Lemma transp_atom_compose x1 x2 y1 y2 z:
  transp_atom x1 x2 (transp_atom y1 y2 z) =
  transp_atom
    (transp_atom x1 x2 y1)
    (transp_atom x1 x2 y2)
    (transp_atom x1 x2 z).
Proof.
  destruct (y1 == z); [| destruct (y2 == z)]; subst.
  - repeat rewrite transp_atom_thisL. reflexivity.
  - repeat rewrite transp_atom_thisR. reflexivity.
  - rewrite (transp_atom_other y1 y2); auto.
    destruct (x1 == z); [| destruct (x2 == z)]; subst.
    + repeat rewrite transp_atom_thisL.
      destruct (x2 == y1); subst.
      × { rewrite transp_atom_thisR.
          destruct (y1 == y2); subst.
          - rewrite transp_atom_thisR. rewrite transp_atom_refl. reflexivity.
          - rewrite (transp_atom_other z y1 y2); auto.
            rewrite (transp_atom_other z y2 y1); auto.
        }
      × { rewrite (transp_atom_other z x2 y1); auto.
          destruct (x2 == y2); subst.
          - rewrite transp_atom_thisR. rewrite transp_atom_other; auto.
          - rewrite (transp_atom_other z x2 y2); auto.
            rewrite transp_atom_other; auto.
        }
    + rewrite transp_atom_thisR.
      destruct (x1 == y1); subst.
      × { rewrite transp_atom_thisL.
          destruct (y1 == y2); subst.
          - rewrite transp_atom_thisL. rewrite transp_atom_refl. reflexivity.
          - rewrite (transp_atom_other y1 z y2); auto.
            rewrite transp_atom_other; auto.
        }
      × { rewrite (transp_atom_other x1 z y1); auto.
          destruct (x1 == y2); subst.
          - rewrite transp_atom_thisL. rewrite transp_atom_other; auto.
          - rewrite (transp_atom_other x1 z y2); auto.
            rewrite transp_atom_other; auto.
        }
    + rewrite (transp_atom_other x1 x2 z); auto.
      destruct (x1 == y1); subst.
      × { rewrite transp_atom_thisL.
          destruct (y1 == y2); subst.
          - rewrite transp_atom_thisL. rewrite transp_atom_refl. reflexivity.
          - destruct (x2 == y2); subst.
            + rewrite transp_atom_thisR. rewrite transp_atom_other; auto.
            + rewrite (transp_atom_other y1 x2 y2); auto.
              rewrite transp_atom_other; auto.
        }
      × { destruct (x2 == y1); subst.
          - rewrite transp_atom_thisR.
            destruct (x1 == y2); subst.
            + rewrite transp_atom_thisL. rewrite transp_atom_other; auto.
            + destruct (y1 == y2); subst.
              × rewrite transp_atom_thisR. rewrite transp_atom_refl. reflexivity.
              × rewrite (transp_atom_other x1 y1 y2); auto.
                rewrite transp_atom_other; auto.
          - rewrite (transp_atom_other x1 x2 y1); auto.
            destruct (x1 == y2); subst.
            + rewrite transp_atom_thisL. rewrite transp_atom_other; auto.
            + destruct (x2 == y2); subst.
              × rewrite transp_atom_thisR. rewrite transp_atom_other; auto.
              × rewrite (transp_atom_other x1 x2 y2); auto.
                rewrite transp_atom_other; auto.
        }
Qed.

Definition atoms_in_dec (x: atom) (S: atoms) : { x `in` S } + { x `notin` S }.
Proof.
  case_eq (AtomSetImpl.mem x S); intros; [left | right].
  - apply mem_iff in H. assumption.
  - intro Hx. apply mem_iff in Hx. congruence.
Qed.

Lemma atoms_eq_antisym (S1 S2: atoms):
  S1 [<=] S2 →
  S2 [<=] S1 →
  S1 [=] S2.
Proof.
  fsetdec.
Qed.

Definition transp_atoms (x y: atom) (S: atoms) : atoms :=
  if atoms_in_dec x S
  then
    if atoms_in_dec y S
    then S
    else add y (remove x S)
  else
    if atoms_in_dec y S
    then add x (remove y S)
    else S.

Add Parametric Morphism: transp_atoms
    with signature eq ==> eq ==> AtomSetImpl.Equal ==> AtomSetImpl.Equal
      as transp_atoms_morphism.
Proof.
  intros x y S1 S2 HS.
  unfold transp_atoms.
  destruct (atoms_in_dec x S1); destruct (atoms_in_dec y S1);
    destruct (atoms_in_dec x S2); destruct (atoms_in_dec y S2);
      fsetdec.
Qed.

Lemma transp_atoms_swap x y S:
  transp_atoms x y S [=] transp_atoms y x S.
Proof.
  unfold transp_atoms.
  destruct (atoms_in_dec x S); destruct (atoms_in_dec y S); fsetdec.
Qed.

Lemma transp_atoms_fresh_eq x y S:
  x `notin` S →
  y `notin` S →
  transp_atoms x y S [=] S.
Proof.
  intros Hx Hy.
  unfold transp_atoms.
  destruct (atoms_in_dec x S); destruct (atoms_in_dec y S); fsetdec.
Qed.

Lemma transp_atoms_not_new_eq x y S:
  x `in` S →
  y `in` S →
  transp_atoms x y S [=] S.
Proof.
  intros Hx Hy.
  unfold transp_atoms.
  destruct (atoms_in_dec x S); destruct (atoms_in_dec y S); fsetdec.
Qed.

Lemma transp_atoms_freshL x y S:
  x `notin` S →
  y `in` S →
  transp_atoms x y S [=] add x (remove y S).
Proof.
  intros Hx Hy.
  unfold transp_atoms.
  destruct (atoms_in_dec x S); destruct (atoms_in_dec y S); fsetdec.
Qed.

Lemma transp_atoms_freshR x y S:
  x `in` S →
  y `notin` S →
  transp_atoms x y S [=] add y (remove x S).
Proof.
  intros Hx Hy.
  unfold transp_atoms.
  destruct (atoms_in_dec x S); destruct (atoms_in_dec y S); fsetdec.
Qed.

Lemma transp_atoms_involution x y S:
  transp_atoms x y (transp_atoms x y S) [=] S.
Proof.
  unfold transp_atoms.
  destruct (atoms_in_dec x S); destruct (atoms_in_dec y S).
  - destruct (atoms_in_dec x S); [| exfalso; fsetdec].
    destruct (atoms_in_dec y S); fsetdec.
  - destruct (atoms_in_dec x (add y (remove x S))); [exfalso; fsetdec |].
    destruct (atoms_in_dec y (add y (remove x S))); fsetdec.
  - destruct (atoms_in_dec x (add x (remove y S))); [| exfalso; fsetdec].
    destruct (atoms_in_dec y (add x (remove y S))); fsetdec.
  - destruct (atoms_in_dec x S); [exfalso; fsetdec |].
    destruct (atoms_in_dec y S); fsetdec.
Qed.

Lemma transp_atoms_refl x S :
  transp_atoms x x S [=] S.
Proof.
  destruct (atoms_in_dec x S); auto using transp_atoms_fresh_eq, transp_atoms_not_new_eq.
Qed.

Lemma in_equivariant x y z S:
  z `in` S ↔ (transp_atom x y z) `in` (transp_atoms x y S).
Proof.
  revert z S.
  assert (∀ z S, z `in` S → (transp_atom x y z) `in` (transp_atoms x y S)).
  { intros z S H.
    unfold transp_atoms.
    destruct (atoms_in_dec x S); destruct (atoms_in_dec y S);
      (destruct (x == z); destruct (y == z); subst;
       [ rewrite transp_atom_refl
       | rewrite transp_atom_thisL
       | rewrite transp_atom_thisR
       | rewrite transp_atom_other
      ]); auto; fsetdec.
  }
  intros z S; split; intro Hz; auto.
  apply H in Hz.
  rewrite transp_atom_involution in Hz.
  rewrite transp_atoms_involution in Hz.
  assumption.
Qed.

Lemma notin_equivariant x y z S:
  z `notin` S ↔ (transp_atom x y z) `notin` (transp_atoms x y S).
Proof.
  split; intros Hn H; apply Hn; clear Hn; [apply in_equivariant in H | apply in_equivariant ]; auto.
Qed.

Lemma atoms_incl_equivariant x y S1 S2:
  S1 [<=] S2 ↔ transp_atoms x y S1 [<=] transp_atoms x y S2.
Proof.
  revert S1 S2.
  assert (∀ S1 S2, S1 [<=] S2 → transp_atoms x y S1 [<=] transp_atoms x y S2).
  { intros S1 S2 H z Hz.
    destruct (atoms_in_dec x S1);
      destruct (atoms_in_dec y S1).
    - rewrite transp_atoms_not_new_eq in Hz; auto.
      rewrite transp_atoms_not_new_eq; auto.
    - rewrite transp_atoms_freshR in Hz; auto.
      destruct (atoms_in_dec y S2).
      + rewrite transp_atoms_not_new_eq; auto. fsetdec.
      + rewrite transp_atoms_freshR; auto. fsetdec.
    - rewrite transp_atoms_freshL in Hz; auto.
      destruct (atoms_in_dec x S2).
      + rewrite transp_atoms_not_new_eq; auto. fsetdec.
      + rewrite transp_atoms_freshL; auto. fsetdec.
    - rewrite transp_atoms_fresh_eq in Hz; auto.
      destruct (atoms_in_dec x S2);
        destruct (atoms_in_dec y S2).
      + rewrite transp_atoms_not_new_eq; auto.
      + rewrite transp_atoms_freshR; auto. fsetdec.
      + rewrite transp_atoms_freshL; auto. fsetdec.
      + rewrite transp_atoms_fresh_eq; auto.
  }
  intros S1 S2; split; intros H12; auto.
  apply H in H12. repeat rewrite transp_atoms_involution in H12. assumption.
Qed.

Lemma atoms_eq_equivariant x y S1 S2:
  S1 [=] S2 ↔ transp_atoms x y S1 [=] transp_atoms x y S2.
Proof.
  revert S1 S2.
  assert (∀ S1 S2, S1 [=] S2 → transp_atoms x y S1 [=] transp_atoms x y S2).
  { intros S1 S2 H.
    apply atoms_eq_antisym.
    - apply atoms_incl_equivariant; auto. fsetdec.
    - apply atoms_incl_equivariant; auto. fsetdec.
  }
  intros S1 S2; split; intro H12; auto.
  apply H in H12. repeat rewrite transp_atoms_involution in H12. assumption.
Qed.

Lemma empty_equivariant x y:
  transp_atoms x y empty [=] empty.
Proof.
  destruct (atoms_in_dec x empty);
    destruct (atoms_in_dec y empty);
    try fsetdec.
  apply transp_atoms_fresh_eq; auto.
Qed.

Lemma singleton_equivariant x y z:
  transp_atoms x y (singleton z) [=] singleton (transp_atom x y z).
Proof.
  destruct (x == z); destruct (y == z); subst.
  - rewrite transp_atoms_refl. rewrite transp_atom_refl. reflexivity.
  - rewrite transp_atoms_freshR; auto. rewrite transp_atom_thisL. fsetdec.
  - rewrite transp_atoms_freshL; auto. rewrite transp_atom_thisR. fsetdec.
  - rewrite transp_atoms_fresh_eq; auto. rewrite transp_atom_other; auto. reflexivity.
Qed.

Lemma union_equivariant x y S1 S2:
  transp_atoms x y (union S1 S2) [=] union (transp_atoms x y S1) (transp_atoms x y S2).
Proof.
  destruct (atoms_in_dec x S1); destruct (atoms_in_dec y S1);
    [ rewrite (transp_atoms_not_new_eq x y S1); auto
    | rewrite (transp_atoms_freshR x y S1); auto
    | rewrite (transp_atoms_freshL x y S1); auto
    | rewrite (transp_atoms_fresh_eq x y S1); auto
    ].
  - destruct (atoms_in_dec x S2); destruct (atoms_in_dec y S2);
      [ rewrite (transp_atoms_not_new_eq x y S2); auto
      | rewrite (transp_atoms_freshR x y S2); auto
      | rewrite (transp_atoms_freshL x y S2); auto
      | rewrite (transp_atoms_fresh_eq x y S2); auto
      ].
    + rewrite transp_atoms_not_new_eq; auto. fsetdec.
    + rewrite transp_atoms_not_new_eq; auto. fsetdec.
    + rewrite transp_atoms_not_new_eq; auto. fsetdec.
    + rewrite transp_atoms_not_new_eq; auto. fsetdec.
  - destruct (atoms_in_dec x S2); destruct (atoms_in_dec y S2);
      [ rewrite (transp_atoms_not_new_eq x y S2); auto
      | rewrite (transp_atoms_freshR x y S2); auto
      | rewrite (transp_atoms_freshL x y S2); auto
      | rewrite (transp_atoms_fresh_eq x y S2); auto
      ].
    + rewrite transp_atoms_not_new_eq; auto. fsetdec.
    + rewrite transp_atoms_freshR; auto. fsetdec.
    + rewrite transp_atoms_not_new_eq; auto. fsetdec.
    + rewrite transp_atoms_freshR; auto. fsetdec.
  - destruct (atoms_in_dec x S2); destruct (atoms_in_dec y S2);
      [ rewrite (transp_atoms_not_new_eq x y S2); auto
      | rewrite (transp_atoms_freshR x y S2); auto
      | rewrite (transp_atoms_freshL x y S2); auto
      | rewrite (transp_atoms_fresh_eq x y S2); auto
      ].
    + rewrite transp_atoms_not_new_eq; auto. fsetdec.
    + rewrite transp_atoms_not_new_eq; auto. fsetdec.
    + rewrite transp_atoms_freshL; auto. fsetdec.
    + rewrite transp_atoms_freshL; auto. fsetdec.
  - destruct (atoms_in_dec x S2); destruct (atoms_in_dec y S2);
      [ rewrite (transp_atoms_not_new_eq x y S2); auto
      | rewrite (transp_atoms_freshR x y S2); auto
      | rewrite (transp_atoms_freshL x y S2); auto
      | rewrite (transp_atoms_fresh_eq x y S2); auto
      ].
    + rewrite transp_atoms_not_new_eq; auto. fsetdec.
    + rewrite transp_atoms_freshR; auto. fsetdec.
    + rewrite transp_atoms_freshL; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
Qed.

Lemma add_equivariant x y z S:
  transp_atoms x y (add z S) [=] add (transp_atom x y z) (transp_atoms x y S).
Proof.
  transitivity (transp_atoms x y (union (singleton z) S)).
  - apply transp_atoms_morphism; auto. fsetdec.
  - rewrite union_equivariant. rewrite singleton_equivariant. fsetdec.
Qed.

Lemma inter_equivariant x y S1 S2:
  transp_atoms x y (inter S1 S2) [=] inter (transp_atoms x y S1) (transp_atoms x y S2).
Proof.
  destruct (atoms_in_dec x S1); destruct (atoms_in_dec y S1);
    [ rewrite (transp_atoms_not_new_eq x y S1); auto
    | rewrite (transp_atoms_freshR x y S1); auto
    | rewrite (transp_atoms_freshL x y S1); auto
    | rewrite (transp_atoms_fresh_eq x y S1); auto
    ].
  - destruct (atoms_in_dec x S2); destruct (atoms_in_dec y S2);
      [ rewrite (transp_atoms_not_new_eq x y S2); auto
      | rewrite (transp_atoms_freshR x y S2); auto
      | rewrite (transp_atoms_freshL x y S2); auto
      | rewrite (transp_atoms_fresh_eq x y S2); auto
      ].
    + rewrite transp_atoms_not_new_eq; auto. fsetdec.
    + rewrite transp_atoms_freshR; auto. fsetdec.
    + rewrite transp_atoms_freshL; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
  - destruct (atoms_in_dec x S2); destruct (atoms_in_dec y S2);
      [ rewrite (transp_atoms_not_new_eq x y S2); auto
      | rewrite (transp_atoms_freshR x y S2); auto
      | rewrite (transp_atoms_freshL x y S2); auto
      | rewrite (transp_atoms_fresh_eq x y S2); auto
      ].
    + rewrite transp_atoms_freshR; auto. fsetdec.
    + rewrite transp_atoms_freshR; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
  - destruct (atoms_in_dec x S2); destruct (atoms_in_dec y S2);
      [ rewrite (transp_atoms_not_new_eq x y S2); auto
      | rewrite (transp_atoms_freshR x y S2); auto
      | rewrite (transp_atoms_freshL x y S2); auto
      | rewrite (transp_atoms_fresh_eq x y S2); auto
      ].
    + rewrite transp_atoms_freshL; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + rewrite transp_atoms_freshL; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
  - destruct (atoms_in_dec x S2); destruct (atoms_in_dec y S2);
      [ rewrite (transp_atoms_not_new_eq x y S2); auto
      | rewrite (transp_atoms_freshR x y S2); auto
      | rewrite (transp_atoms_freshL x y S2); auto
      | rewrite (transp_atoms_fresh_eq x y S2); auto
      ].
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
Qed.

Lemma diff_equivariant x y S1 S2:
  transp_atoms x y (diff S1 S2) [=] diff (transp_atoms x y S1) (transp_atoms x y S2).
Proof.
  destruct (atoms_in_dec x S1); destruct (atoms_in_dec y S1);
    [ rewrite (transp_atoms_not_new_eq x y S1); auto
    | rewrite (transp_atoms_freshR x y S1); auto
    | rewrite (transp_atoms_freshL x y S1); auto
    | rewrite (transp_atoms_fresh_eq x y S1); auto
    ].
  - destruct (atoms_in_dec x S2); destruct (atoms_in_dec y S2);
      [ rewrite (transp_atoms_not_new_eq x y S2); auto
      | rewrite (transp_atoms_freshR x y S2); auto
      | rewrite (transp_atoms_freshL x y S2); auto
      | rewrite (transp_atoms_fresh_eq x y S2); auto
      ].
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + rewrite transp_atoms_freshL; auto. fsetdec.
    + rewrite transp_atoms_freshR; auto. fsetdec.
    + rewrite transp_atoms_not_new_eq; auto. fsetdec.
  - destruct (atoms_in_dec x S2); destruct (atoms_in_dec y S2);
      [ rewrite (transp_atoms_not_new_eq x y S2); auto
      | rewrite (transp_atoms_freshR x y S2); auto
      | rewrite (transp_atoms_freshL x y S2); auto
      | rewrite (transp_atoms_fresh_eq x y S2); auto
      ].
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + rewrite transp_atoms_freshR; auto. fsetdec.
    + rewrite transp_atoms_freshR; auto. fsetdec.
  - destruct (atoms_in_dec x S2); destruct (atoms_in_dec y S2);
      [ rewrite (transp_atoms_not_new_eq x y S2); auto
      | rewrite (transp_atoms_freshR x y S2); auto
      | rewrite (transp_atoms_freshL x y S2); auto
      | rewrite (transp_atoms_fresh_eq x y S2); auto
      ].
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + rewrite transp_atoms_freshL; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + rewrite transp_atoms_freshL; auto. fsetdec.
  - destruct (atoms_in_dec x S2); destruct (atoms_in_dec y S2);
      [ rewrite (transp_atoms_not_new_eq x y S2); auto
      | rewrite (transp_atoms_freshR x y S2); auto
      | rewrite (transp_atoms_freshL x y S2); auto
      | rewrite (transp_atoms_fresh_eq x y S2); auto
      ].
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + rewrite transp_atoms_fresh_eq; auto. fsetdec.
Qed.

Lemma remove_equivariant x y z S:
  transp_atoms x y (remove z S) [=] remove (transp_atom x y z) (transp_atoms x y S).
Proof.
  transitivity (transp_atoms x y (diff S (singleton z))).
  - apply atoms_eq_equivariant. fsetdec.
  - rewrite diff_equivariant. rewrite singleton_equivariant. fsetdec.
Qed.

Lemma transp_atoms_trans x1 x2 x3 S:
  x1 `notin` S →
  x2 `notin` S →
  transp_atoms x1 x2 (transp_atoms x2 x3 S) [=] transp_atoms x1 x3 S.
Proof.
  intros H1 H2.
  destruct (atoms_in_dec x3 S).
  - rewrite (transp_atoms_freshL x1 x3); auto.
    rewrite (transp_atoms_freshL x2 x3); auto.
    rewrite add_equivariant. rewrite transp_atom_thisR.
    rewrite remove_equivariant.
    rewrite transp_atoms_fresh_eq; auto.
    rewrite transp_atom_other; fsetdec.
  - rewrite (transp_atoms_fresh_eq x1 x3); auto.
    rewrite (transp_atoms_fresh_eq x2 x3); auto.
    rewrite (transp_atoms_fresh_eq x1 x2); auto.
    fsetdec.
Qed.

Lemma transp_atoms_compose x1 x2 y1 y2 S:
  transp_atoms x1 x2 (transp_atoms y1 y2 S) [=]
  transp_atoms
    (transp_atom x1 x2 y1)
    (transp_atom x1 x2 y2)
    (transp_atoms x1 x2 S).
Proof.
  destruct (x1 == x2); subst.
  - repeat rewrite transp_atom_refl.
    repeat rewrite transp_atoms_refl.
    reflexivity.
  - destruct (atoms_in_dec y1 S); destruct (atoms_in_dec y2 S);
      [ rewrite (transp_atoms_not_new_eq y1 y2 S); auto
      | rewrite (transp_atoms_freshR y1 y2 S); auto
      | rewrite (transp_atoms_freshL y1 y2 S); auto
      | rewrite (transp_atoms_fresh_eq y1 y2 S); auto
      ];
      (destruct (atoms_in_dec x1 S); destruct (atoms_in_dec x2 S);
       [ rewrite (transp_atoms_not_new_eq x1 x2 S); auto
       | rewrite (transp_atoms_freshR x1 x2 S); auto
       | rewrite (transp_atoms_freshL x1 x2 S); auto
       | rewrite (transp_atoms_fresh_eq x1 x2 S); auto
       ]
      );
      try repeat rewrite add_equivariant;
      try repeat rewrite remove_equivariant.
    + rewrite transp_atoms_not_new_eq; [ fsetdec | | ].
      × destruct (x1 == y1); destruct (x2 == y1); subst;
          [ contradiction
          | rewrite transp_atom_thisL; auto
          | rewrite transp_atom_thisR; auto
          | rewrite transp_atom_other; auto
          ].
      × destruct (x1 == y2); destruct (x2 == y2); subst;
          [ contradiction
          | rewrite transp_atom_thisL; auto
          | rewrite transp_atom_thisR; auto
          | rewrite transp_atom_other; auto
          ].
    + destruct (x1 == y1); subst.
      × { repeat rewrite transp_atom_thisL.
          destruct (y1 == y2); subst.
          - rewrite transp_atom_thisL.
            rewrite transp_atom_refl. rewrite transp_atoms_refl. fsetdec.
          - rewrite (transp_atom_other y1 x2); auto; try fsetdec.
            rewrite (transp_atom_other x2 y2); auto; try fsetdec.
            rewrite transp_atoms_freshL; auto. fsetdec.
        }
      × { rewrite (transp_atom_other x1 x2 y1); auto; try fsetdec.
          destruct (x1 == y2); subst.
          - rewrite transp_atom_thisL. rewrite transp_atom_thisR.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite transp_atoms_freshR; auto. fsetdec.
          - rewrite (transp_atom_other x1 x2); auto; try fsetdec.
            rewrite (transp_atom_other y1 y2 x2); auto; try fsetdec.
            rewrite (transp_atom_other y1 y2 x1); auto; try fsetdec.
            rewrite transp_atoms_not_new_eq; auto. fsetdec.
        }
    + destruct (x2 == y1); subst.
      × { rewrite transp_atom_thisR. rewrite transp_atom_thisL.
          destruct (y1 == y2); subst.
          - rewrite transp_atom_thisR.
            rewrite transp_atom_refl. rewrite transp_atoms_refl. fsetdec.
          - rewrite (transp_atom_other x1 y1 y2); auto; try fsetdec.
            rewrite (transp_atom_other x1 y2 y1); auto; try fsetdec.
            rewrite transp_atoms_freshL; auto. fsetdec.
        }
      × { rewrite (transp_atom_other x1 x2 y1); auto; try fsetdec.
          destruct (x2 == y2); subst.
          - repeat rewrite transp_atom_thisR.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite transp_atoms_freshR; auto. fsetdec.
          - rewrite (transp_atom_other x1 x2 y2); auto; try fsetdec.
            rewrite (transp_atom_other y1 y2 x1); auto; try fsetdec.
            rewrite (transp_atom_other y1 y2 x2); auto; try fsetdec.
            rewrite transp_atoms_not_new_eq; auto. fsetdec.
        }
    + rewrite transp_atom_other; try fsetdec.
      rewrite transp_atom_other; try fsetdec.
      rewrite transp_atoms_not_new_eq; auto. fsetdec.
    + rewrite transp_atoms_not_new_eq; auto.
      destruct (x2 == y2); subst.
      × { rewrite transp_atom_thisR.
          destruct (x1 == y1); subst.
          - rewrite transp_atom_thisL. rewrite transp_atoms_freshL; auto. fsetdec.
          - rewrite transp_atom_other; auto. rewrite transp_atoms_not_new_eq; auto. fsetdec.
        }
      × { rewrite (transp_atom_other x1 x2 y2); auto; try fsetdec.
          destruct (x1 == y1); destruct (x2 == y1); subst; try contradiction.
          - rewrite transp_atom_thisL. rewrite transp_atoms_freshR; auto. fsetdec.
          - rewrite transp_atom_thisR. rewrite transp_atoms_freshR; auto. fsetdec.
          - rewrite transp_atom_other; auto. rewrite transp_atoms_freshR; auto. fsetdec.
        }
    + destruct (x2 == y2); subst.
      × { repeat rewrite transp_atom_thisR.
          destruct (x1 == y1); subst.
          - repeat rewrite transp_atom_thisL.
            rewrite (transp_atoms_swap y1 y2). fsetdec.
          - rewrite transp_atom_other; auto; try fsetdec.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite (transp_atoms_freshR x1 y2); auto.
            rewrite (transp_atoms_not_new_eq y1 x1); auto.
            fsetdec.
        }
      × { rewrite (transp_atom_other x1 x2); auto; try fsetdec.
          destruct (x1 == y1); subst.
          - repeat rewrite transp_atom_thisL.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite (transp_atoms_freshR y1 x2); auto.
            rewrite (transp_atoms_fresh_eq x2 y2); auto.
            fsetdec.
          - rewrite (transp_atom_other x1 x2 y1); auto; try fsetdec.
            rewrite (transp_atom_other y1 y2 x2); auto; try fsetdec.
            rewrite (transp_atom_other y1 y2 x1); auto; try fsetdec.
            rewrite (transp_atoms_freshR x1 x2); auto.
            rewrite (transp_atoms_freshR y1 y2); auto.
            fsetdec.
        }
    + destruct (x1 == y2); subst.
      × { rewrite transp_atom_thisL. rewrite transp_atom_thisR.
          destruct (x2 == y1); subst.
          - repeat rewrite transp_atom_thisR. rewrite transp_atom_thisL.
            rewrite (transp_atoms_freshL y2 y1); auto. fsetdec.
          - rewrite (transp_atom_other y2 x2 y1); auto; try fsetdec.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite (transp_atoms_freshL y2 x2); auto.
            rewrite (transp_atoms_not_new_eq y1 x2); auto.
            fsetdec.
        }
      × { rewrite (transp_atom_other x1 x2 y2); auto; try fsetdec.
          destruct (x2 == y1); subst.
          - rewrite transp_atom_thisR. rewrite transp_atom_thisL.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite (transp_atoms_freshL x1 y1); auto.
            rewrite (transp_atoms_fresh_eq x1 y2); auto.
            fsetdec.
          - rewrite (transp_atom_other x1 x2 y1); auto; try fsetdec.
            rewrite (transp_atom_other y1 y2 x1); auto; try fsetdec.
            rewrite (transp_atom_other y1 y2 x2); auto; try fsetdec.
            rewrite (transp_atoms_freshL x1 x2); auto.
            rewrite (transp_atoms_freshR y1 y2); auto.
            fsetdec.
        }
    + destruct (x1 == y2); destruct (x2 == y2); subst; try contradiction.
      × rewrite transp_atom_thisL.
        rewrite transp_atom_other; auto; try fsetdec.
        rewrite (transp_atoms_fresh_eq y2 x2); auto.
        rewrite (transp_atoms_freshR y1 x2); auto.
        fsetdec.
      × rewrite transp_atom_thisR.
        rewrite transp_atom_other; auto; try fsetdec.
        rewrite (transp_atoms_fresh_eq x1 y2); auto.
        rewrite (transp_atoms_freshR y1 x1); auto.
        fsetdec.
      × rewrite (transp_atom_other x1 x2 y2); auto.
        rewrite transp_atom_other; auto; try fsetdec.
        rewrite (transp_atoms_fresh_eq x1 x2); auto.
        rewrite (transp_atoms_freshR y1 y2); auto.
        fsetdec.
    + rewrite (transp_atom_other x1 x2 y1); auto; try fsetdec.
      destruct (x1 == y2); destruct (x2 == y2); subst; try contradiction.
      × rewrite transp_atom_thisL.
        rewrite (transp_atoms_not_new_eq y2 x2); auto.
        rewrite (transp_atoms_freshL y1 x2); auto.
        fsetdec.
      × rewrite transp_atom_thisR.
        rewrite (transp_atoms_not_new_eq x1 y2); auto.
        rewrite (transp_atoms_freshL y1 x1); auto.
        fsetdec.
      × rewrite transp_atom_other; auto.
        rewrite (transp_atoms_not_new_eq x1 x2); auto.
        rewrite (transp_atoms_freshL y1 y2); auto.
        fsetdec.
    + destruct (x2 == y1); subst.
      × { rewrite transp_atom_thisR. rewrite transp_atom_thisL.
          destruct (x1 == y2); subst.
          - rewrite transp_atom_thisL. rewrite transp_atom_thisR.
            rewrite (transp_atoms_freshR y2 y1); auto. fsetdec.
          - rewrite transp_atom_other; auto; try fsetdec.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite (transp_atoms_freshR x1 y1); auto.
            rewrite (transp_atoms_not_new_eq x1 y2); auto.
            fsetdec.
        }
      × { rewrite (transp_atom_other x1 x2 y1); auto; try fsetdec.
          destruct (x1 == y2); subst.
          - rewrite transp_atom_thisL. rewrite transp_atom_thisR.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite (transp_atoms_freshR y2 x2); auto.
            rewrite (transp_atoms_fresh_eq y1 x2); auto. fsetdec.
          - rewrite (transp_atom_other x1 x2 y2); auto; try fsetdec.
            rewrite (transp_atom_other y1 y2 x2); auto; try fsetdec.
            rewrite (transp_atom_other y1 y2 x1); auto; try fsetdec.
            rewrite (transp_atoms_freshR x1 x2); auto.
            rewrite (transp_atoms_freshL y1 y2); auto.
            fsetdec.
        }
    + destruct (x1 == y1); subst.
      × { repeat rewrite transp_atom_thisL.
          destruct (x2 == y2); subst.
          - repeat rewrite transp_atom_thisR.
            rewrite (transp_atoms_swap y1 y2); auto. fsetdec.
          - rewrite (transp_atom_other y1 x2 y2); auto; try fsetdec.
            rewrite (transp_atom_other x2 y2 y1); auto; try fsetdec.
            rewrite (transp_atoms_freshL y1 x2); auto.
            rewrite (transp_atoms_not_new_eq x2 y2); auto.
            fsetdec.
        }
      × { rewrite (transp_atom_other x1 x2 y1); auto; try fsetdec.
          destruct (x2 == y2); subst.
          - repeat rewrite transp_atom_thisR.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite (transp_atoms_freshL x1 y2); auto.
            rewrite (transp_atoms_fresh_eq y1 x1); auto.
            fsetdec.
          - rewrite (transp_atom_other x1 x2 y2); auto; try fsetdec.
            rewrite (transp_atom_other y1 y2 x1); auto; try fsetdec.
            rewrite (transp_atom_other y1 y2 x2); auto; try fsetdec.
            rewrite (transp_atoms_freshL x1 x2); auto.
            rewrite (transp_atoms_freshL y1 y2); auto.
            fsetdec.
        }
    + destruct (x1 == y1); destruct (x2 == y1); subst; try contradiction.
      × rewrite transp_atom_thisL.
        rewrite transp_atom_other; auto; try fsetdec.
        rewrite (transp_atoms_fresh_eq y1 x2); auto.
        rewrite (transp_atoms_freshL x2 y2); auto.
        fsetdec.
      × rewrite transp_atom_thisR.
        rewrite transp_atom_other; auto; try fsetdec.
        rewrite (transp_atoms_fresh_eq x1 y1); auto.
        rewrite (transp_atoms_freshL x1 y2); auto.
        fsetdec.
      × rewrite (transp_atom_other x1 x2 y1); auto.
        rewrite transp_atom_other; auto; try fsetdec.
        rewrite (transp_atoms_fresh_eq x1 x2); auto.
        rewrite (transp_atoms_freshL y1 y2); auto.
        fsetdec.
    + rewrite transp_atom_other; try fsetdec.
      rewrite transp_atom_other; try fsetdec.
      rewrite transp_atoms_fresh_eq; auto. fsetdec.
    + destruct (x2 == y1); subst.
      × { rewrite transp_atom_thisR. rewrite transp_atom_thisL.
          destruct (y1 == y2); subst.
          - rewrite transp_atom_thisR.
            rewrite transp_atom_refl. rewrite transp_atoms_refl.
            fsetdec.
          - rewrite (transp_atom_other x1 y1 y2); auto; try fsetdec.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite transp_atoms_freshR; auto.
            fsetdec.
        }
      × { rewrite (transp_atom_other x1 x2 y1); auto; try fsetdec.
          destruct (x2 == y2); subst.
          - repeat rewrite transp_atom_thisR.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite transp_atoms_freshL; auto. fsetdec.
          - rewrite (transp_atom_other x1 x2 y2); auto; try fsetdec.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite transp_atoms_fresh_eq; auto. fsetdec.
        }
    + destruct (x1 == y1); subst.
      × { repeat rewrite transp_atom_thisL.
          destruct (y1 == y2); subst.
          - rewrite transp_atom_thisL.
            rewrite transp_atom_refl. rewrite transp_atoms_refl. fsetdec.
          - rewrite (transp_atom_other y1 x2 y2); auto; try fsetdec.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite transp_atoms_freshR; auto. fsetdec.
        }
      × { rewrite (transp_atom_other x1 x2 y1); auto; try fsetdec.
          destruct (x1 == y2); subst.
          - rewrite transp_atom_thisL. rewrite transp_atom_thisR.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite transp_atoms_freshL; auto. fsetdec.
          - rewrite (transp_atom_other x1 x2 y2); auto; try fsetdec.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite transp_atom_other; auto; try fsetdec.
            rewrite transp_atoms_fresh_eq; auto. fsetdec.
        }
    + destruct (x1 == y1); destruct (x2 == y1); subst; try contradiction.
      × { rewrite transp_atom_thisL.
          destruct (y1 == y2); destruct (x2 == y2); subst; try contradiction.
          - rewrite transp_atom_thisL.
            rewrite transp_atoms_fresh_eq; auto. fsetdec.
          - rewrite transp_atom_thisR.
            rewrite transp_atoms_fresh_eq; auto. fsetdec.
          - rewrite transp_atom_other; auto.
            rewrite transp_atoms_fresh_eq; auto. fsetdec.
        }
      × { rewrite transp_atom_thisR.
          destruct (x1 == y2); destruct (y1 == y2); subst; try contradiction.
          - rewrite transp_atom_thisL.
            rewrite transp_atoms_fresh_eq; auto. fsetdec.
          - rewrite transp_atom_thisR.
            rewrite transp_atoms_fresh_eq; auto. fsetdec.
          - rewrite transp_atom_other; auto.
            rewrite transp_atoms_fresh_eq; auto. fsetdec.
        }
      × { rewrite (transp_atom_other x1 x2 y1); auto.
          destruct (x1 == y2); destruct (x2 == y2); subst; try contradiction.
          - rewrite transp_atom_thisL.
            rewrite transp_atoms_fresh_eq; auto. fsetdec.
          - rewrite transp_atom_thisR.
            rewrite transp_atoms_fresh_eq; auto. fsetdec.
          - rewrite transp_atom_other; auto.
            rewrite transp_atoms_fresh_eq; auto. fsetdec.
        }
Qed.

Fixpoint transp_dom {A} y x (e: env A) :=
  match e with
  | nil ⇒ nil
  | (z, a) :: e ⇒ (transp_atom y x z, a) :: transp_dom y x e
  end.

Lemma transp_dom_map {A B} x y (f: A → B) (e: env A) :
  map f (transp_dom x y e) = transp_dom x y (map f e).
Proof.
  env induction e; simpl; auto.
  f_equal. assumption.
Qed.

Lemma transp_dom_app {A} y x (e1 e2: env A) :
  transp_dom y x (e1 ++ e2) = transp_dom y x e1 ++ transp_dom y x e2.
Proof.
  env induction e1; simpl; simpl_env; congruence.
Qed.

Lemma transp_dom_length {A} y x (e: env A) :
  length (transp_dom y x e) = length e.
Proof.
  env induction e; simpl; auto.
Qed.

Lemma transp_dom_swap {A} x y (e: env A):
  transp_dom x y e = transp_dom y x e.
Proof.
  env induction e; simpl; auto.
  rewrite transp_atom_swap. congruence.
Qed.

Lemma dom_equivariant {A} x y (e: env A):
  transp_atoms x y (dom e) [=] dom (transp_dom x y e).
Proof.
  env induction e; simpl.
  - apply empty_equivariant.
  - rewrite add_equivariant. rewrite IHe. reflexivity.
Qed.

Lemma transp_dom_fresh_eq {A} x y (e: env A):
  x `notin` dom e →
  y `notin` dom e →
  transp_dom x y e = e.
Proof.
  intros Hx Hy. env induction e; simpl; auto.
  rewrite transp_atom_other; auto. rewrite IHe; auto.
Qed.

Lemma transp_dom_refl {A} x (e: env A) :
  transp_dom x x e = e.
Proof.
  env induction e; simpl; auto.
  rewrite transp_atom_refl. congruence.
Qed.

Lemma transp_dom_trans {A} x1 x2 x3 (e: env A) :
  x1 `notin` dom e →
  x2 `notin` dom e →
  transp_dom x1 x2 (transp_dom x2 x3 e) = transp_dom x1 x3 e.
Proof.
  intros H1 H2.
  env induction e; simpl in *; auto.
  rewrite transp_atom_trans; auto.
  rewrite IHe; auto.
Qed.

Lemma transp_dom_involution {A} x y (e: env A):
  transp_dom x y (transp_dom x y e) = e.
Proof.
  env induction e; simpl; auto.
  rewrite transp_atom_involution. congruence.
Qed.

Lemma transp_dom_compose {A} x1 x2 y1 y2 (e: env A):
  transp_dom x1 x2 (transp_dom y1 y2 e) =
  transp_dom
    (transp_atom x1 x2 y1)
    (transp_atom x1 x2 y2)
    (transp_dom x1 x2 e).
Proof.
  env induction e; simpl; auto.
  rewrite transp_atom_compose. congruence.
Qed.

Lemma get_transp_dom_equivariant {A} x y z (e: env A):
  get z e = get (transp_atom x y z) (transp_dom x y e).
Proof.
  env induction e; simpl; auto.
  destruct (z == x0); subst.
  - destruct (transp_atom x y x0 == transp_atom x y x0); congruence.
  - destruct (transp_atom x y z == transp_atom x y x0).
    + exfalso. apply n.
      rewrite <- (transp_atom_involution x y z).
      rewrite e. rewrite transp_atom_involution. reflexivity.
    + assumption.
Qed.

Lemma get_transp_dom_Some_equivariant {A} x y z a (e: env A):
  get z e = Some a ↔ get (transp_atom x y z) (transp_dom x y e) = Some a.
Proof.
  rewrite <- get_transp_dom_equivariant. tauto.
Qed.

Lemma get_transp_dom_None_equivariant {A} x y z (e: env A):
  get z e = None ↔ get (transp_atom x y z) (transp_dom x y e) = None.
Proof.
  rewrite <- get_transp_dom_equivariant. tauto.
Qed.

Lemma get_transp_dom_this {A} x y (e: env A):
  y `notin` dom e →
  get y (transp_dom x y e) = get x e.
Proof.
  assert (x `notin` dom e ∨ x `in` dom e) as [Hx|Hx] by fsetdec.
  - intro Hy. rewrite transp_dom_fresh_eq; auto.
    apply get_notin_dom in Hx.
    apply get_notin_dom in Hy.
    congruence.
  - intros Hy. env induction e; simpl; auto.
    destruct (x == x0); subst.
    + rewrite transp_atom_thisL. destruct (y == y); congruence.
    + simpl in Hx. simpl in Hy. rewrite transp_atom_other; auto.
      destruct (y == x0); subst.
      × exfalso. fsetdec.
      × rewrite IHe; auto. fsetdec.
Qed.

Lemma get_transp_dom_old {A} x y (e: env A):
  y `notin` dom e →
  y ≠ x →
  get x (transp_dom x y e) = get y e.
Proof.
  intros Hy Hneq. env induction e; simpl; auto.
  destruct (y == x0); subst.
  - rewrite transp_atom_thisR. destruct (x == x); congruence.
  - simpl in Hy.
    rewrite IHe; auto.
    destruct (x == x0); subst.
    + rewrite transp_atom_thisL. destruct (x0 == y); congruence.
    + rewrite transp_atom_other; auto. destruct (x == x0); congruence.
Qed.

Lemma get_transp_dom_old_removed {A} x y (e: env A):
  y `notin` dom e →
  y ≠ x →
  get x (transp_dom x y e) = None.
Proof.
  intros Hy Hneq.
  rewrite get_transp_dom_old; auto.
  apply get_notin_dom. auto.
Qed.

Lemma get_transp_dom_other {A} z x y (e: env A):
  z ≠ y →
  z ≠ x →
  get z (transp_dom x y e) = get z e.
Proof.
  intros Hz1 Hz2. env induction e; simpl; auto.
  rewrite IHe. clear IHe.
  destruct (z == x0); subst.
  - rewrite transp_atom_other; auto. destruct (x0 == x0); congruence.
  - destruct (x == x0); [| destruct (y == x0)]; subst.
    + rewrite transp_atom_thisL. destruct (z == y); congruence.
    + rewrite transp_atom_thisR. destruct (z == x); congruence.
    + rewrite transp_atom_other; auto. destruct (z == x0); congruence.
Qed.

Lemma get_transp_dom {A} x y z (e: env A):
  y `notin` dom e →
  get (transp_atom x y z) (transp_dom x y e) = get z e.
Proof.
  intro Hy.
  destruct (x == z); [| destruct (y == z)]; subst.
  - rewrite transp_atom_thisL. rewrite get_transp_dom_this; auto.
  - rewrite transp_atom_thisR. rewrite get_transp_dom_old; auto.
  - rewrite transp_atom_other; auto. rewrite get_transp_dom_other; auto.
Qed.

Lemma in_transp_dom_equivariant {A} x y z a (e: env A):
  In (z, a) e ↔ In (transp_atom x y z, a) (transp_dom x y e).
Proof.
  revert z a e.
  assert (∀ z a (e: env A), In (z, a) e → In (transp_atom x y z, a) (transp_dom x y e)).
  { intros z a e Hz. env induction e; simpl in *; auto; try contradiction.
    destruct Hz as [Hz|Hz]; [left|right].
    - congruence.
    - auto.
  }
  intros z a e. split; intro Hz; auto.
  apply H in Hz.
  rewrite transp_atom_involution in Hz.
  rewrite transp_dom_involution in Hz.
  assumption.
Qed.

Lemma in_transp_dom_this {A} x y a (e: env A):
  y `notin` dom e →
  In (y, a) (transp_dom x y e) ↔ In (x, a) e.
Proof.
  assert (x `notin` dom e ∨ x `in` dom e) as [Hx|Hx] by fsetdec.
  - intro Hy. rewrite transp_dom_fresh_eq; auto.
    split; intro Hin; apply in_in_dom in Hin; exfalso; fsetdec.
  - intros Hy. revert a. env induction e; intros; simpl in *; auto.
    + tauto.
    + split.
      × { intros [H|H].
          - inversion H; subst. clear H.
            destruct (x == x0); subst.
            + left. reflexivity.
            + destruct (y == x0); subst.
              × rewrite transp_atom_thisR in H1. contradiction.
              × rewrite transp_atom_other in H1; auto. subst.
                exfalso. fsetdec.
          - assert (x `in` dom xs ∨ x `notin` dom xs) as [?|?] by fsetdec.
            + right. apply IHe; auto.
            + exfalso. assert (x = x0) by fsetdec. subst.
              rewrite transp_dom_fresh_eq in H; auto.
              apply in_in_dom in H. fsetdec.
        }
      × { intros [H|H].
          - inversion H; subst. clear H.
            rewrite transp_atom_thisL. left. reflexivity.
          - assert (x `in` dom xs ∨ x `notin` dom xs) as [?|?] by fsetdec.
            + right. apply IHe; auto.
            + exfalso. assert (x = x0) by fsetdec. subst.
              apply in_in_dom in H. fsetdec.
        }
Qed.

Lemma in_transp_dom_old {A} x y a (e: env A):
  y `notin` dom e →
  y ≠ x →
  In (x, a) (transp_dom x y e) ↔ In (y, a) e.
Proof.
  intros Hy Hneq. revert a. env induction e; intros; simpl in *; auto.
  - tauto.
  - split.
    + intros [H|H].
      × { inversion H; subst. clear H.
          destruct (x == x0); subst.
          - rewrite transp_atom_thisL in H1. contradiction.
          - rewrite transp_atom_other in H1; auto. congruence.
        }
      × apply IHe in H; auto.
    + intros [H|H].
      × inversion H; subst. clear H.
        rewrite transp_atom_thisR. left. reflexivity.
      × apply IHe in H; auto.
Qed.

Lemma in_transp_dom_old_removed {A} x y a (e: env A):
  y `notin` dom e →
  y ≠ x →
  ¬ In (x, a) (transp_dom x y e).
Proof.
  intros Hy Hneq.
  rewrite in_transp_dom_old; auto.
  intro H. apply in_in_dom in H. fsetdec.
Qed.

Lemma in_transp_dom_other {A} z x y a (e: env A):
  z ≠ y →
  z ≠ x →
  In (z, a) (transp_dom x y e) ↔ In (z, a) e.
Proof.
  intros Hz1 Hz2. revert a. env induction e; intros; simpl; auto.
  - tauto.
  - rewrite IHe. clear IHe.
    destruct (z == x0); subst.
    + rewrite transp_atom_other; auto. tauto.
    + destruct (x == x0); [| destruct (y == x0)]; subst.
      × { rewrite transp_atom_thisL. split.
          - intros [H|H].
            + congruence.
            + right. assumption.
          - intros [H|H].
            + congruence.
            + right. assumption.
        }
      × { rewrite transp_atom_thisR. split.
          - intros [H|H].
            + congruence.
            + right. assumption.
          - intros [H|H].
            + congruence.
            + right. assumption.
        }
      × rewrite transp_atom_other; auto. tauto.
Qed.

Lemma in_transp_dom {A} x y z a (e: env A):
  y `notin` dom e →
  In ((transp_atom x y z), a) (transp_dom x y e) ↔ In (z, a) e.
Proof.
  intro Hy.
  destruct (x == z); [| destruct (y == z)]; subst.
  - rewrite transp_atom_thisL. rewrite in_transp_dom_this; tauto.
  - rewrite transp_atom_thisR. rewrite in_transp_dom_old; auto. tauto.
  - rewrite transp_atom_other; auto. rewrite in_transp_dom_other; auto. tauto.
Qed.