Require Import Transp.
Require Import Infrastructure.
Require Import Env.
Require Import SubstEnv.
Require Import Rel.
Require Import RelGood.
Require Import RelStable.

Lemma all_env_term_equivariant (P: term → Prop):
  (∀ x y t, P (transp_term x y t) ↔ P t) →
  ∀ x y e, all_env P (transp_env_term x y e) ↔ all_env P e.
Proof.
  intros HP x y e. env induction e; simpl in ×.
  - tauto.
  - rewrite HP; auto. rewrite IHe. reflexivity.
Qed.

Lemma all_env_rel_equivariant (P: rel (env term) term → Prop):
  (∀ x y t, P (transp_rel x y t) ↔ P t) →
  ∀ x y e, all_env P (transp_env_rel x y e) ↔ all_env P e.
Proof.
  intros HP x y e. env induction e; simpl in ×.
  - tauto.
  - rewrite HP; auto. rewrite IHe. reflexivity.
Qed.

Lemma lc_equivariant x y t:
  lc (transp_term x y t) ↔ lc t.
Proof.
  revert t.
  assert (∀ t, lc t → lc (transp_term x y t)).
  { intros t H. induction H; simpl; auto.
    - constructor; auto. intro z.
      specialize (H1 (transp_atom x y z)).
      rewrite open_equivariant in H1. simpl in H1.
      rewrite transp_atom_involution in H1. assumption.
    - constructor; auto. intro z.
      specialize (H0 (transp_atom x y z)).
      rewrite open_equivariant in H0. simpl in H0.
      rewrite transp_atom_involution in H0. assumption.
    - constructor; auto.
      + intro z.
        specialize (H1 (transp_atom x y z)).
        rewrite open_equivariant in H1. simpl in H1.
        rewrite transp_atom_involution in H1. assumption.
      + intro z.
        specialize (H3 (transp_atom x y z)).
        rewrite open_equivariant in H3. simpl in H3.
        rewrite transp_atom_involution in H3. assumption.
  }
  intro t; split; intro Ht; auto.
  apply H in Ht. rewrite transp_term_involution in Ht. assumption.
Qed.

Lemma is_value_equivariant x y t:
  is_value (transp_term x y t) ↔ is_value t.
Proof.
  induction t; simpl; tauto.
Qed.

Lemma is_extended_value_equivariant x y t:
  is_extended_value (transp_term x y t) ↔ is_extended_value t.
Proof.
  induction t; simpl; tauto.
Qed.

Lemma closed_term_equivariant x y t:
  fv (transp_term x y t) [<=] empty ↔ fv t [<=] empty.
Proof.
  rewrite (atoms_incl_equivariant x y).
  rewrite fv_equivariant. rewrite transp_term_involution. rewrite empty_equivariant.
  reflexivity.
Qed.

Lemma good_value_equivariant x y t:
  good_value (transp_term x y t) ↔ good_value t.
Proof.
  split; intros [Hlc [Hvalue Hclosed]]; (split; [| split]);
    try solve [ eapply lc_equivariant; eauto
              | eapply is_value_equivariant; eauto
              | eapply closed_term_equivariant; eauto
              ].
Qed.

Lemma leq_env_equivariant x y e1 e2:
  leq_env e1 e2 ↔ leq_env (transp_env_term x y e1) (transp_env_term x y e2).
Proof.
  revert e1 e2.
  assert (∀ e1 e2, leq_env e1 e2 → leq_env (transp_env_term x y e1) (transp_env_term x y e2)).
  { intros e1 e2 H z v Hzv.
    assert (get (transp_atom x y z) e1 = Some (transp_term x y v)).
    { rewrite (get_transp_env_term_Some_equivariant x y) in Hzv.
      rewrite transp_env_term_involution in Hzv.
      assumption.
    }
    apply H in H0.
    rewrite (get_transp_env_term_Some_equivariant x y) in H0.
    rewrite transp_atom_involution in H0.
    rewrite transp_term_involution in H0.
    assumption.
  }
  intros e1 e2. split; intro H'; auto.
  apply H in H'. repeat rewrite transp_env_term_involution in H'. assumption.
Qed.

Lemma good_rel_equivariant x y R:
  good_rel R ↔ good_rel (transp_rel x y R).
Proof.
  revert R.
  assert (∀ R, good_rel R → good_rel (transp_rel x y R)).
  { intros R H e v Hev.
    apply H in Hev. destruct Hev as [Hegood Hvgood].
    apply all_env_term_equivariant in Hegood; auto using good_value_equivariant.
    apply good_value_equivariant in Hvgood.
    tauto.
  }
  intro R; split; intro HR; auto.
  apply H in HR. rewrite transp_rel_involution in HR.
  assumption.
Qed.

Lemma stable_equivariant x y R:
  stable_rel R ↔ stable_rel (transp_rel x y R).
Proof.
  revert R.
  assert (∀ R, stable_rel R → stable_rel (transp_rel x y R)).
  { intros R H e v Hev.
    apply H in Hev.
    intros e' Hgood' Hleq. simpl.
    apply Hev.
    - apply all_env_term_equivariant; auto using good_value_equivariant.
    - apply leq_env_equivariant; auto.
  }
  intro R; split; intro HR; auto.
  apply H in HR. rewrite transp_rel_involution in HR.
  assumption.
Qed.

Lemma dom_rel_equivariant_rel x y S (R: rel (env term) term) :
  dom_rel (transp_atoms x y S) (transp_rel x y R) ↔ dom_rel S R.
Proof.
  revert S R.
  assert (∀ (S : atoms) (R : rel (env term) term),
             dom_rel S R → dom_rel (transp_atoms x y S) (transp_rel x y R)) as H.
  { intros S R H. intros e v Hev.
    apply (atoms_incl_equivariant x y).
    rewrite transp_atoms_involution.
    rewrite dom_equivariant_term.
    simpl in Hev.
    eapply H; eauto.
  }
  intros S R. split; intro H0; auto.
  apply H in H0.
  rewrite transp_atoms_involution in H0.
  rewrite transp_rel_involution in H0.
  assumption.
Qed.

Lemma step_equivariant x y t1 t2:
  step t1 t2 ↔ step (transp_term x y t1) (transp_term x y t2).
Proof.
  revert t1 t2.
  assert (∀ t1 t2, step t1 t2 → step (transp_term x y t1) (transp_term x y t2)).
  { intros t1 t2 H.
    induction H; simpl;
      try solve [ try rewrite open_equivariant;
                  constructor; auto;
                  try solve [ apply is_value_equivariant; auto ] ].
  }
  intros t1 t2; split; intro H12; auto.
  apply H in H12. repeat rewrite transp_term_involution in H12. assumption.
Qed.

Lemma steps_equivariant x y t1 t2:
  steps t1 t2 ↔ steps (transp_term x y t1) (transp_term x y t2).
Proof.
  revert t1 t2.
  assert (∀ t1 t2, steps t1 t2 → steps (transp_term x y t1) (transp_term x y t2)).
  { intros t1 t2 H.
    induction H.
    - constructor.
    - econstructor; eauto.
      rewrite <- step_equivariant. assumption.
  }
  intros t1 t2; split; intro H12; auto.
  apply H in H12. repeat rewrite transp_term_involution in H12. assumption.
Qed.

Lemma eval_equivariant x y t1 t2:
  eval t1 t2 ↔ eval (transp_term x y t1) (transp_term x y t2).
Proof.
  revert t1 t2.
  assert (∀ t1 t2, eval t1 t2 → eval (transp_term x y t1) (transp_term x y t2)).
  { intros t1 t2 [Hsteps Hval]. split.
    - rewrite <- steps_equivariant. assumption.
    - apply is_value_equivariant. assumption.
  }
  intros t1 t2; split; intro H12; auto.
  apply H in H12. repeat rewrite transp_term_involution in H12. assumption.
Qed.

Lemma RelIncl_rel_equivariant x y R1 R2:
  RelIncl R1 R2 ↔ RelIncl (transp_rel x y R1) (transp_rel x y R2).
Proof.
  revert R1 R2.
  assert (∀ R1 R2, RelIncl R1 R2 → RelIncl (transp_rel x y R1) (transp_rel x y R2)).
  { intros R1 R2 H12 e v H. simpl in ×. apply H12. assumption. }
  intros R1 R2; split; intro H12; auto.
  apply H in H12.
  repeat rewrite transp_rel_involution in H12.
  assumption.
Qed.

Lemma RelIncl_vrel_equivariant x y R1 R2:
  RelIncl R1 R2 ↔ RelIncl (transp_vrel x y R1) (transp_vrel x y R2).
Proof.
  revert R1 R2.
  assert (∀ R1 R2, RelIncl R1 R2 → RelIncl (transp_vrel x y R1) (transp_vrel x y R2)).
  { intros R1 R2 H12 e v H. simpl in ×. apply H12. assumption. }
  intros R1 R2; split; intro H12; auto.
  apply H in H12.
  repeat rewrite transp_vrel_involution in H12.
  assumption.
Qed.

Lemma RelEquiv_rel_equivariant x y R1 R2:
  RelEquiv R1 R2 ↔ RelEquiv (transp_rel x y R1) (transp_rel x y R2).
Proof.
  split; intro; apply RelIncl_antisym.
  - rewrite <- (RelIncl_rel_equivariant x y); auto.
  - rewrite <- (RelIncl_rel_equivariant x y); auto.
  - apply (RelIncl_rel_equivariant x y); auto.
  - apply (RelIncl_rel_equivariant x y); auto.
Qed.

Lemma RelEquiv_vrel_equivariant x y R1 R2:
  RelEquiv R1 R2 ↔ RelEquiv (transp_vrel x y R1) (transp_vrel x y R2).
Proof.
  split; intro; apply RelIncl_antisym.
  - rewrite <- (RelIncl_vrel_equivariant x y); auto.
  - rewrite <- (RelIncl_vrel_equivariant x y); auto.
  - apply (RelIncl_vrel_equivariant x y); auto.
  - apply (RelIncl_vrel_equivariant x y); auto.
Qed.

Lemma RelBot_rel_equivariant x y:
  RelEquiv (transp_rel x y RelBot) RelBot.
Proof.
  intros e v. simpl. tauto.
Qed.

Lemma RelBot_vrel_equivariant x y:
  RelEquiv (transp_vrel x y RelBot) RelBot.
Proof.
  intros v1 v2. simpl. tauto.
Qed.

Lemma RelTopEnvVal_rel_equivariant x y:
  RelEquiv (transp_rel x y RelTopEnvVal) RelTopEnvVal.
Proof.
  intros e v; split; intros [Hegood Hvgood]; split.
  - rewrite all_env_term_equivariant in Hegood; auto using good_value_equivariant.
  - apply good_value_equivariant in Hvgood; auto.
  - rewrite all_env_term_equivariant; auto using good_value_equivariant.
  - apply good_value_equivariant; auto.
Qed.

Lemma RelTopVal_vrel_equivariant x y:
  RelEquiv (transp_vrel x y RelTopVal) RelTopVal.
Proof.
  intros v1 v2; split; intros [H1 H2]; split.
  - apply good_value_equivariant in H1; auto.
  - apply good_value_equivariant in H2; auto.
  - apply good_value_equivariant; auto.
  - apply good_value_equivariant; auto.
Qed.

Lemma RelEqVal_vrel_equivariant x y:
  RelEquiv (transp_vrel x y RelEqVal) RelEqVal.
Proof.
  intros v1 v2; split; intros [H1 H2]; split.
  - rewrite <- (transp_term_involution x y v1). rewrite H1.
    rewrite transp_term_involution. reflexivity.
  - apply good_value_equivariant in H2; auto.
  - congruence.
  - apply good_value_equivariant; auto.
Qed.

Lemma RelInter_rel_equivariant x y R1 R2:
  RelEquiv
    (transp_rel x y (RelInter R1 R2))
    (RelInter (transp_rel x y R1) (transp_rel x y R2)).
Proof.
  intros e v. reflexivity.
Qed.

Lemma RelInter_vrel_equivariant x y R1 R2:
  RelEquiv
    (transp_vrel x y (RelInter R1 R2))
    (RelInter (transp_vrel x y R1) (transp_vrel x y R2)).
Proof.
  intros e v. reflexivity.
Qed.

Lemma RelUnion_rel_equivariant x y R1 R2:
  RelEquiv
    (transp_rel x y (RelUnion R1 R2))
    (RelUnion (transp_rel x y R1) (transp_rel x y R2)).
Proof.
  intros e v. reflexivity.
Qed.

Lemma RelUnion_vrel_equivariant x y R1 R2:
  RelEquiv
    (transp_vrel x y (RelUnion R1 R2))
    (RelUnion (transp_vrel x y R1) (transp_vrel x y R2)).
Proof.
  intros e v. reflexivity.
Qed.

Lemma RelCompose_rel_equivariant x y R1 R2:
  RelEquiv
    (transp_rel x y (RelCompose R1 R2))
    (RelCompose (transp_rel x y R1) (transp_vrel x y R2)).
Proof.
  intros e v; split; intros [v' [Hev' Hv'v]]; simpl in ×.
  - ∃ (transp_term x y v'). split; rewrite transp_term_involution; assumption.
  - ∃ (transp_term x y v'). split; assumption.
Qed.

Lemma RelCompose_RelInv_rel_equivariant x y R1 R2:
  RelEquiv
    (transp_vrel x y (RelCompose (RelInv R1) R2))
    (RelCompose (RelInv (transp_rel x y R1)) (transp_rel x y R2)).
Proof.
  intros v1 v2; split; intros [e [Hv1e Hev2]]; simpl in ×.
  - ∃ (transp_env_term x y e). split; rewrite transp_env_term_involution; assumption.
  - ∃ (transp_env_term x y e). split; assumption.
Qed.

Lemma RelCompose_vrel_equivariant x y R1 R2:
  RelEquiv
    (transp_vrel x y (RelCompose R1 R2))
    (RelCompose (transp_vrel x y R1) (transp_vrel x y R2)).
Proof.
  intros e v; split; intros [v' [Hev' Hv'v]]; simpl in ×.
  - ∃ (transp_term x y v'). split; rewrite transp_term_involution; assumption.
  - ∃ (transp_term x y v'). split; assumption.
Qed.

Lemma RelUnitR_rel_equivariant x y:
  RelEquiv (transp_rel x y RelUnitR) RelUnitR.
Proof.
  intros e v; split; intro Hev; simpl in *; destruct v; simpl in *; try contradiction.
  - eapply all_env_term_equivariant; eauto using good_value_equivariant.
  - eapply all_env_term_equivariant; eauto using good_value_equivariant.
Qed.

Lemma RelPairR_rel_equivariant x y R1 R2:
  RelEquiv
    (transp_rel x y (RelPairR R1 R2))
    (RelPairR (transp_rel x y R1) (transp_rel x y R2)).
Proof.
  intros e v; split; intro Hev; simpl in *; destruct v; simpl in *; tauto.
Qed.

Lemma RelPairR_vrel_equivariant x y R1 R2:
  RelEquiv
    (transp_vrel x y (RelPairR R1 R2))
    (RelPairR (transp_vrel x y R1) (transp_vrel x y R2)).
Proof.
  intros v1 v2; split; intro Hev; simpl in *; destruct v2; simpl in *; tauto.
Qed.

Lemma RelPairL_vrel_equivariant x y R1 R2:
  RelEquiv
    (transp_vrel x y (RelPairL R1 R2))
    (RelPairL (transp_vrel x y R1) (transp_vrel x y R2)).
Proof.
  intros v1 v2; split; intro Hev; simpl in *; destruct v1; simpl in *; tauto.
Qed.

Lemma RelSumR_rel_equivariant x y R1 R2:
  RelEquiv
    (transp_rel x y (RelSumR R1 R2))
    (RelSumR (transp_rel x y R1) (transp_rel x y R2)).
Proof.
  intros e v; split; intro Hev; simpl in *; destruct v; simpl in *; tauto.
Qed.

Lemma RelSumR_vrel_equivariant x y R1 R2:
  RelEquiv
    (transp_vrel x y (RelSumR R1 R2))
    (RelSumR (transp_vrel x y R1) (transp_vrel x y R2)).
Proof.
  intros v1 v2; split; intro Hev; simpl in *; destruct v2; simpl in *; tauto.
Qed.

Lemma RelSumL_vrel_equivariant x y R1 R2:
  RelEquiv
    (transp_vrel x y (RelSumL R1 R2))
    (RelSumL (transp_vrel x y R1) (transp_vrel x y R2)).
Proof.
  intros v1 v2; split; intro Hev; simpl in *; destruct v1; simpl in *; tauto.
Qed.

Lemma RelGather_rel_equivariant x y E:
  RelEquiv
    (transp_rel x y (RelGather E))
    (RelGather (transp_env_rel x y E)).
Proof.
  intros e v. split; intros [Hall [Hgood Hself]]; (split; [| split ]).
  - eapply all_env_term_equivariant; eauto using good_value_equivariant.
  - eapply good_value_equivariant; eauto.
  - intros z R Hz.
    apply get_transp_env_rel_Some_equivariant_inv in Hz.
    destruct Hz as [R' [Hz Hequiv]].
    apply Hself in Hz.
    destruct Hz as [v' [Hz Hv']].
    ∃ (transp_term x y v'). split.
    + apply (get_transp_env_term_Some_equivariant x y) in Hz.
      rewrite transp_atom_involution in Hz.
      rewrite transp_env_term_involution in Hz.
      assumption.
    + rewrite Hequiv in Hv'.
      simpl in Hv'. rewrite transp_env_term_involution in Hv'.
      assumption.
  - eapply all_env_term_equivariant; eauto using good_value_equivariant.
  - eapply good_value_equivariant; eauto.
  - intros z R Hz.
    apply (get_transp_env_rel_Some_equivariant x y) in Hz.
    apply Hself in Hz.
    destruct Hz as [v' [Hz' HR]].
    ∃ (transp_term x y v'). split.
    + apply (get_transp_env_term_Some_equivariant x y) in Hz'.
      rewrite transp_atom_involution in Hz'. assumption.
    + assumption.
Qed.

Lemma RelSelf_rel_equivariant x y t:
  RelEquiv
    (transp_rel x y (RelSelf t))
    (RelSelf (transp_term x y t)).
Proof.
  intros e v. split; intros [Hsubst [Hfv [Hegood Hvgood]]]; (split; [| split; [| split ]]).
  - rewrite <- (transp_term_involution x y v).
    rewrite <- Hsubst.
    rewrite subst_env_equivariant.
    rewrite transp_env_term_involution.
    reflexivity.
  - rewrite (atoms_incl_equivariant x y) in Hfv.
    rewrite fv_equivariant in Hfv. rewrite dom_equivariant_term in Hfv.
    rewrite transp_env_term_involution in Hfv. assumption.
  - eapply all_env_term_equivariant; eauto using good_value_equivariant.
  - eapply good_value_equivariant; eauto.
  - rewrite <- Hsubst.
    rewrite <- (transp_env_term_involution x y e).
    rewrite subst_env_equivariant.
    rewrite transp_term_involution.
    reflexivity.
  - rewrite (atoms_incl_equivariant x y) in Hfv.
    rewrite fv_equivariant in Hfv. rewrite dom_equivariant_term in Hfv.
    rewrite transp_term_involution in Hfv. assumption.
  - eapply all_env_term_equivariant; eauto using good_value_equivariant.
  - eapply good_value_equivariant; eauto.
Qed.

Lemma FUN_rel_equivariant x y S R1 R2:
  RelEquiv
    (transp_rel x y (FUN S R1 R2))
    (FUN (transp_atoms x y S) (transp_rel x y R1) (transp_rel x y R2)).
Proof.
  intros e v; split; intros [Hedom [Hegood [Hvgood H]]]; (split; [| split; [| split]]).
  - apply (atoms_incl_equivariant x y) in Hedom.
    rewrite dom_equivariant_term in Hedom. rewrite transp_env_term_involution in Hedom.
    assumption.
  - apply all_env_term_equivariant in Hegood; auto using good_value_equivariant.
  - apply good_value_equivariant in Hvgood; auto.
  - intros e' Hleq v1 H' v2 Heval.
    simpl in ×.
    apply (leq_env_equivariant x y) in Hleq.
    apply (eval_equivariant x y) in Heval.
    simpl in Heval.
    eauto.
  - apply (atoms_incl_equivariant x y) in Hedom.
    rewrite transp_atoms_involution in Hedom. rewrite dom_equivariant_term in Hedom.
    assumption.
  - apply all_env_term_equivariant; auto using good_value_equivariant.
  - apply good_value_equivariant; auto.
  - intros e' Hleq v1 H' v2 Heval.
    simpl in ×.
    rewrite <- (transp_env_term_involution x y e').
    rewrite <- (transp_term_involution x y).
    apply H with (v1 := transp_term x y v1); auto.
    + apply (leq_env_equivariant x y) in Hleq.
      rewrite transp_env_term_involution in Hleq.
      assumption.
    + rewrite transp_env_term_involution.
      rewrite transp_term_involution.
      assumption.
    + apply (eval_equivariant x y) in Heval. simpl in Heval.
      rewrite transp_term_involution in Heval.
      assumption.
Qed.

Lemma APP_rel_equivariant x y R1 R2:
  RelEquiv
    (transp_rel x y (APP R1 R2))
    (APP (transp_rel x y R1) (transp_rel x y R2)).
Proof.
  intros e v; split; intros [e' [v1 [v2 [Hleq [H1 [H2 Heval]]]]]]; simpl in ×.
  - ∃ (transp_env_term x y e'), (transp_term x y v1), (transp_term x y v2).
    split; [| split; [| split]].
    + apply (leq_env_equivariant x y) in Hleq.
      rewrite transp_env_term_involution in Hleq.
      assumption.
    + rewrite transp_env_term_involution.
      rewrite transp_term_involution.
      assumption.
    + rewrite transp_term_involution.
      assumption.
    + apply (eval_equivariant x y) in Heval. simpl in Heval.
      rewrite transp_term_involution in Heval.
      assumption.
  - ∃ (transp_env_term x y e'), (transp_term x y v1), (transp_term x y v2).
    split; [| split; [| split]].
    + apply leq_env_equivariant; auto.
    + assumption.
    + assumption.
    + apply (eval_equivariant x y) in Heval; assumption.
Qed.

Lemma depFUN_rel_equivariant x y S R1 R2:
  RelEquiv
    (transp_rel x y (depFUN S R1 R2))
    (depFUN (transp_atoms x y S) (transp_rel x y R1) (fun v ⇒ transp_rel x y (R2 (transp_term x y v)))).
Proof.
  intros e v; split; intros [Hedom [Hegood [Hvgood H]]]; (split; [| split; [| split]]).
  - apply (atoms_incl_equivariant x y) in Hedom.
    rewrite dom_equivariant_term in Hedom. rewrite transp_env_term_involution in Hedom.
    assumption.
  - apply all_env_term_equivariant in Hegood; auto using good_value_equivariant.
  - apply good_value_equivariant in Hvgood; auto.
  - intros e' Hleq v1 H' v2 Heval.
    simpl in ×.
    apply (leq_env_equivariant x y) in Hleq.
    apply (eval_equivariant x y) in Heval.
    simpl in Heval.
    eauto.
  - apply (atoms_incl_equivariant x y) in Hedom.
    rewrite transp_atoms_involution in Hedom. rewrite dom_equivariant_term in Hedom.
    assumption.
  - apply all_env_term_equivariant; auto using good_value_equivariant.
  - apply good_value_equivariant; auto.
  - intros e' Hleq v1 H' v2 Heval.
    simpl in ×.
    rewrite <- (transp_env_term_involution x y e').
    rewrite <- (transp_term_involution x y v1).
    rewrite <- (transp_term_involution x y v2).
    apply H with (v1 := transp_term x y v1); auto.
    + apply (leq_env_equivariant x y) in Hleq.
      rewrite transp_env_term_involution in Hleq.
      assumption.
    + rewrite transp_env_term_involution.
      rewrite transp_term_involution.
      assumption.
    + apply (eval_equivariant x y) in Heval. simpl in Heval.
      rewrite transp_term_involution in Heval.
      assumption.
Qed.

Lemma RelLet0_strong_rel_equivariant x y R1 R2 S:
  FamilyRelEquiv S
    (transp_family_rel x y (RelLet0_strong R1 R2))
    (RelLet0_strong (transp_family_rel x y R1) (transp_rel x y R2)).
Proof.
  intros z Hz e v. split; intros [v' [H2 H1]]; simpl in ×.
  - ∃ (transp_term x y v'). split.
    + rewrite transp_term_involution.
      assumption.
    + unfold transp_env_term. simpl.
      rewrite transp_term_involution.
      assumption.
  - ∃ (transp_term x y v'). split.
    + assumption.
    + unfold transp_env_term in H1. simpl in H1.
      assumption.
Qed.

Lemma RelClose_rel_equivariant x y S R:
  RelEquiv
    (transp_rel x y (RelClose S R))
    (RelClose (transp_atoms x y S) (transp_family_rel x y R)).
Proof.
  intros e v. split; intros [z [HS Hz]]; simpl in ×.
  - ∃ (transp_atom x y z). split.
    + apply notin_equivariant. assumption.
    + rewrite transp_atom_involution. assumption.
  - ∃ (transp_atom x y z). split.
    + apply (notin_equivariant x y) in HS. rewrite transp_atoms_involution in HS.
      assumption.
    + assumption.
Qed.

Lemma RelLet_strong_rel_equivariant x y S R1 R2:
  RelEquiv
    (transp_rel x y (RelLet_strong S R1 R2))
    (RelLet_strong (transp_atoms x y S) (transp_family_rel x y R1) (transp_rel x y R2)).
Proof.
  unfold RelLet_strong.
  rewrite RelClose_rel_equivariant.
  rewrite RelLet0_strong_rel_equivariant.
  reflexivity.
Qed.

Lemma RelRemove_rel_equivariant x y R1 R2 z :
  RelEquiv (transp_rel x y (RelRemove R1 R2 z))
           (RelRemove (transp_rel x y R1) (transp_rel x y R2) (transp_atom x y z)).
Proof.
  intros e v; split; intros [v' [H2 H1]]; simpl in *; simpl_env in ×.
  - ∃ (transp_term x y v'). split.
    + rewrite transp_term_involution. assumption.
    + simpl_env. rewrite transp_env_term_app. rewrite transp_env_term_one.
      rewrite transp_atom_involution. rewrite transp_term_involution.
      assumption.
  - ∃ (transp_term x y v'). split.
    + assumption.
    + rewrite transp_env_term_app in H1. rewrite transp_env_term_one in H1.
      rewrite transp_atom_involution in H1.
      assumption.
Qed.

Lemma RelCompose_RelPush_equivariant x y R1 z v R2 :
  RelEquiv (transp_rel x y (RelCompose (RelPush R1 z v) R2))
           (RelCompose (RelPush (transp_rel x y R1)
                                (transp_atom x y z)
                                (transp_term x y v)
                       )
                       (transp_rel x y R2)
           ).
Proof.
  revert R1 z v R2.
  assert (∀ R1 z v R2,
             RelIncl (transp_rel x y (RelCompose (RelPush R1 z v) R2))
                     (RelCompose (RelPush (transp_rel x y R1)
                                          (transp_atom x y z)
                                          (transp_term x y v)
                                 )
                                 (transp_rel x y R2)
                     )
         ).
  { intros R1 z v R2 e v' [v1 [[Heq H1] H2]]. subst.
    apply (in_rel_equivariant x y) in H1.
    rewrite transp_env_term_involution in H1.
    apply (in_rel_equivariant x y) in H2.
    rewrite transp_env_term_app in H2.
    rewrite transp_env_term_one in H2.
    rewrite transp_env_term_involution in H2.
    rewrite transp_term_involution in H2.
    ∃ ((transp_atom x y z) ¬ (transp_term x y v) ++ e).
    split.
    - split; [ reflexivity | assumption ].
    - assumption.
  }
  intros R1 z v R2 e v'. split; intro H0; auto.
  - apply H. assumption.
  - apply (in_rel_equivariant x y) in H0.
    apply H in H0.
    repeat rewrite transp_rel_involution in H0.
    rewrite transp_atom_involution in H0.
    repeat rewrite transp_term_involution in H0.
    assumption.
Qed.

Lemma remove_all_equivariant_term x y z e:
  transp_env_term x y (remove_all z e) =
  remove_all (transp_atom x y z) (transp_env_term x y e).
Proof.
  env induction e; simpl.
  - reflexivity.
  - destruct (x0 == z); subst.
    + destruct (transp_atom x y z == transp_atom x y z); [ | contradiction ].
      assumption.
    + destruct (transp_atom x y x0 == transp_atom x y z).
      × exfalso. apply n. clear n.
        rewrite <- (transp_atom_involution x y x0).
        rewrite e. apply transp_atom_involution.
      × simpl_env. rewrite transp_env_term_app. rewrite transp_env_term_one.
        rewrite IHe. reflexivity.
Qed.

Lemma leq_env_transp_present_bindings1 x1 v1 x2 v2 e:
  all_env (fun v ⇒ fv v [<=] empty) e →
  leq_env (x1 ¬ v1 ++ x2 ¬ v2 ++ e)
          (x1 ¬ v1 ++ x2 ¬ v2 ++ transp_env_term x1 x2 e).
Proof.
  intros He x3 v3 Hget.
  simpl in Hget. simpl.
  destruct (x3 == x1); try subst x3; auto.
  destruct (x3 == x2); try subst x3; auto.
  assert (fv v3 [<=] empty) as Hfv3.
  { apply (all_env_get _ _ _ _ He) in Hget; auto. }
  apply (get_transp_env_term_Some_equivariant x1 x2) in Hget.
  rewrite transp_atom_other in Hget; auto.
  rewrite transp_term_fresh_eq in Hget.
  - assumption.
  - rewrite Hfv3. auto.
  - rewrite Hfv3. auto.
Qed.

Lemma leq_env_transp_present_bindings2 x1 v1 x2 v2 e:
  all_env (fun v ⇒ fv v [<=] empty) e →
  leq_env (x1 ¬ v1 ++ x2 ¬ v2 ++ transp_env_term x1 x2 e)
          (x1 ¬ v1 ++ x2 ¬ v2 ++ e).
Proof.
  intros He x3 v3 Hget.
  simpl in Hget. simpl.
  destruct (x3 == x1); try subst x3; auto.
  destruct (x3 == x2); try subst x3; auto.
  assert (fv v3 [<=] empty) as Hfv3.
  { eapply (all_env_term_equivariant _ closed_term_equivariant x1 x2) in He.
    apply (all_env_get _ _ _ _ He) in Hget; auto.
  }
  apply (get_transp_env_term_Some_equivariant x1 x2).
  rewrite transp_atom_other; auto.
  rewrite transp_term_fresh_eq.
  - assumption.
  - rewrite Hfv3. auto.
  - rewrite Hfv3. auto.
Qed.