Require Import Infrastructure.
Import Notations.
Require Import Env.
Require Import Rel.
Require Import Transp.
Require Import EquivarianceFacts.
Require Import SupportFacts.
Require Import RelExtra.
Require Import Interp.
Require Import RelWf.
Require Import Perm.

Lemma Interp_equivariant_strong E t (Hlc: lc t) (Hfv: fv t [<=] dom E):
  well_supported_env E →
  ∀ pi E' t' (Hlc': lc t') (Hfv': fv t' [<=] dom E'),
    env_rel_equiv E' (perm_env_rel pi E) →
    t' = perm_term pi t →
    RelEquiv (Interp E' t' Hlc' Hfv') (perm_rel pi (Interp E t Hlc Hfv)).
Proof.
  apply Interp_ind; clear E t Hlc Hfv; intros.
  - rewrite perm_Var in H1. subst.
    destruct (Interp_equations _ _ Hlc' Hfv') as [Rx [Hgetx Heq]].
    rewrite Heq. clear Heq.
    rewrite H0.
    rewrite perm_RelInter.
    rewrite perm_RelSelf. rewrite perm_Var.
    rewrite perm_RelGather.
    reflexivity.
  - rewrite perm_Let in H1. subst.
    destruct (Interp_equations _ _ Hlc' Hfv') as [y [Hy [t2' [Heqt2 [Hlc1' [Hfv1' [Hlc2' [Hfv2' Heq]]]]]]]].
    rewrite Heq. clear Heq.
    assert (perm_atom pi x `notin` dom E') as Hx'.
    { apply (perm_notin pi) in Hx. rewrite perm_dom in Hx.
      rewrite H0. assumption.
    }
    rewrite perm_RelLet.
    simpl.
    rewrite perm_dom. rewrite <- H0.
    assert (RelEquiv (Interp E' (perm_term pi t1) Hlc1' Hfv1')
                     (perm_rel pi (Interp E t1 Hlc1 Hfv1)))
      as Hequiv1.
    { apply IH1; auto. }
    rewrite (RelLet_bound_var_rename _ (perm_atom pi x) y); auto.
    + apply RelLet_morphism_equiv; try reflexivity; try assumption.
      rewrite <- perm_rel_snoc. apply IH2.
      × split; auto with supported_rel.
      × { assert (well_supported_env E').
          { rewrite H0. apply perm_well_supported_env. assumption. }
          rewrite perm_env_rel_app. rewrite perm_env_rel_one. simpl. split; [| split ].
          - rewrite perm_atom_snoc. rewrite transp_atom_thisL. reflexivity.
          - rewrite perm_rel_snoc. rewrite <- Hequiv1.
            rewrite transp_rel_fresh_eq with (S := dom E'); auto with supported_rel.
            reflexivity.
          - rewrite perm_env_rel_snoc. rewrite <- H0.
            rewrite transp_env_rel_fresh_eq with (S := dom E'); auto with supported_rel.
            reflexivity.
        }
      × rewrite perm_term_snoc.
        rewrite perm_close in Heqt2.
        apply close_inverse in Heqt2.
        symmetry. assumption.
    + rewrite H0. rewrite <- perm_dom. apply perm_supported_rel.
      auto with supported_rel.
    + rewrite H0. rewrite <- perm_dom. rewrite <- perm_add.
      apply perm_supported_rel.
      apply Interp_supported with (E := (x, Interp E t1 Hlc1 Hfv1) :: E).
      split; auto with supported_rel.
  - rewrite perm_Lam in H1. subst.
    destruct (Interp_equations _ _ Hlc' Hfv') as [y [Hy [t1' [Heqt1 [Hlc1' [Hfv1' Heq]]]]]].
    rewrite Heq. clear Heq.
    assert (perm_atom pi x `notin` dom E') as Hx'.
    { apply (perm_notin pi) in Hx. rewrite perm_dom in Hx.
      rewrite H0. assumption.
    }
    repeat rewrite perm_RelInter.
    rewrite perm_RelLam.
    rewrite perm_RelTopEnvVal.
    rewrite perm_RelSelf.
    rewrite perm_RelGather.
    simpl.
    rewrite perm_dom. rewrite <- H0.
    apply RelInter_morphism_equiv.
    + rewrite (RelLam_bound_var_rename _ (perm_atom pi x) y); auto.
      × { apply RelLam_morphism_equiv; try reflexivity; try assumption.
          rewrite <- perm_rel_snoc. apply IH1.
          - split; auto with supported_rel.
          - { assert (well_supported_env E').
              { rewrite H0. apply perm_well_supported_env. assumption. }
              rewrite perm_env_rel_app. rewrite perm_env_rel_one.
              simpl. split; [| split ].
              - rewrite perm_atom_snoc. rewrite transp_atom_thisL. reflexivity.
              - rewrite perm_rel_snoc. rewrite perm_RelTopEnvVal.
                rewrite transp_rel_fresh_eq with (S := dom E'); auto with supported_rel.
                reflexivity.
              - rewrite perm_env_rel_snoc. rewrite <- H0.
                rewrite transp_env_rel_fresh_eq with (S := dom E');
                  auto with supported_rel.
                reflexivity.
            }
          - rewrite perm_term_snoc.
            rewrite perm_close in Heqt1.
            apply close_inverse in Heqt1.
            symmetry. assumption.
        }
      × auto with good_rel.
      × auto with supported_rel.
      × rewrite H0. rewrite <- perm_dom. rewrite <- perm_add.
        apply perm_supported_rel.
        apply Interp_supported with (E := (x, RelTopEnvVal) :: E).
        split; auto with supported_rel.
    + rewrite perm_Lam. rewrite Heqt1. reflexivity.
  - rewrite perm_App in H1. subst.
    destruct (Interp_equations _ _ Hlc' Hfv') as [Hlc1' [Hfv1' [Hlc2' [Hfv2' Heq]]]].
    rewrite Heq. clear Heq.
    rewrite perm_APP.
    simpl.
    apply APP_morphism_equiv; try reflexivity; try assumption.
    + apply IH1; auto.
    + apply IH2; auto.
  - rewrite perm_Unit in H1. subst.
    pose proof (Interp_equations _ _ Hlc' Hfv') as Heq. simpl in Heq.
    rewrite Heq. clear Heq.
    rewrite perm_RelInter.
    rewrite perm_RelUnitR.
    rewrite perm_RelGather. rewrite H0.
    reflexivity.
  - rewrite perm_Pair in H1. subst.
    destruct (Interp_equations _ _ Hlc' Hfv') as [Hlc1' [Hfv1' [Hlc2' [Hfv2' Heq]]]].
    rewrite Heq. clear Heq.
    rewrite perm_RelPairR.
    simpl.
    apply RelPairR_morphism_equiv; try reflexivity; try assumption.
    + apply IH1; auto.
    + apply IH2; auto.
  - rewrite perm_Fst in H1. subst.
    destruct (Interp_equations _ _ Hlc' Hfv') as [Hlc1' [Hfv1' Heq]].
    rewrite Heq. clear Heq.
    rewrite perm_RelCompose.
    rewrite perm_RelPairL. rewrite perm_RelEqVal. rewrite perm_RelTopVal.
    simpl.
    apply RelCompose_morphism_equiv; try reflexivity; try assumption.
    apply IH1; auto.
  - rewrite perm_Snd in H1. subst.
    destruct (Interp_equations _ _ Hlc' Hfv') as [Hlc1' [Hfv1' Heq]].
    rewrite Heq. clear Heq.
    rewrite perm_RelCompose.
    rewrite perm_RelPairL. rewrite perm_RelEqVal. rewrite perm_RelTopVal.
    simpl.
    apply RelCompose_morphism_equiv; try reflexivity; try assumption.
    apply IH1; auto.
  - rewrite perm_InjL in H1. subst.
    destruct (Interp_equations _ _ Hlc' Hfv') as [Hlc1' [Hfv1' Heq]].
    rewrite Heq. clear Heq.
    rewrite perm_RelSumR. rewrite perm_RelBot.
    simpl.
    apply RelSumR_morphism_equiv; try reflexivity; try assumption.
    apply IH1; auto.
  - rewrite perm_InjR in H1. subst.
    destruct (Interp_equations _ _ Hlc' Hfv') as [Hlc1' [Hfv1' Heq]].
    rewrite Heq. clear Heq.
    rewrite perm_RelSumR. rewrite perm_RelBot.
    simpl.
    apply RelSumR_morphism_equiv; try reflexivity; try assumption.
    apply IH1; auto.
  - rewrite perm_Match in H1. subst.
    destruct (Interp_equations _ _ Hlc' Hfv') as [y2 [Hy2 [t2' [Heqt2 [y3 [Hy3 [t3' [Heqt3 [Hlc1' [Hfv1' [Hlc2' [Hfv2' [Hlc3' [Hfv3' Heq]]]]]]]]]]]]]].
    rewrite Heq. clear Heq.
    assert (perm_atom pi x2 `notin` dom E') as Hx2'.
    { apply (perm_notin pi) in Hx2. rewrite perm_dom in Hx2.
      rewrite H0. assumption.
    }
    assert (perm_atom pi x3 `notin` dom E') as Hx3'.
    { apply (perm_notin pi) in Hx3. rewrite perm_dom in Hx3.
      rewrite H0. assumption.
    }
    rewrite perm_RelUnion.
    repeat rewrite perm_RelLet.
    repeat rewrite perm_RelCompose.
    simpl.
    rewrite perm_dom. rewrite <- H0.
    assert (RelEquiv (Interp E' (perm_term pi t1) Hlc1' Hfv1')
                     (perm_rel pi (Interp E t1 Hlc1 Hfv1)))
      as Hequiv1.
    { apply IH1; auto. }
    assert (well_supported_env E').
    { rewrite H0. apply perm_well_supported_env. assumption. }
    apply RelUnion_morphism_equiv.
    + rewrite (RelLet_bound_var_rename _ (perm_atom pi x2) y2); auto.
      × { apply RelLet_morphism_equiv; try reflexivity; try assumption.
          - apply RelCompose_morphism_equiv.
            + assumption.
            + rewrite perm_RelSumL. rewrite perm_RelEqVal. rewrite perm_RelBot_vrel.
              reflexivity.
          - rewrite <- perm_rel_snoc. apply IH2.
            + split; auto with supported_rel.
            + { rewrite perm_env_rel_app. rewrite perm_env_rel_one. simpl. split; [| split ].
                - rewrite perm_atom_snoc. rewrite transp_atom_thisL. reflexivity.
                - rewrite perm_rel_snoc. rewrite perm_RelCompose.
                  rewrite perm_RelSumL. rewrite perm_RelEqVal. rewrite perm_RelBot_vrel.
                  rewrite <- Hequiv1.
                  rewrite transp_rel_fresh_eq with (S := dom E'); auto with supported_rel.
                  reflexivity.
                - rewrite perm_env_rel_snoc. rewrite <- H0.
                  rewrite transp_env_rel_fresh_eq with (S := dom E'); auto with supported_rel.
                  reflexivity.
              }
            + rewrite perm_term_snoc.
              rewrite perm_close in Heqt2.
              apply close_inverse in Heqt2.
              symmetry. assumption.
        }
      × rewrite H0. rewrite <- perm_dom.
        rewrite perm_RelSumL. rewrite perm_RelEqVal. rewrite perm_RelBot_vrel.
        apply RelCompose_supported_rel; auto with supported_rel.
        apply perm_supported_rel. auto with supported_rel.
      × rewrite H0. rewrite <- perm_dom. rewrite <- perm_add.
        apply perm_supported_rel.
        apply Interp_supported with (E := (x2, RelCompose (Interp E t1 Hlc1 Hfv1) (RelSumL RelEqVal RelBot)) :: E).
        split; auto with supported_rel.
    + rewrite (RelLet_bound_var_rename _ (perm_atom pi x3) y3); auto.
      × { apply RelLet_morphism_equiv; try reflexivity; try assumption.
          - apply RelCompose_morphism_equiv.
            + assumption.
            + rewrite perm_RelSumL. rewrite perm_RelEqVal. rewrite perm_RelBot_vrel.
              reflexivity.
          - rewrite <- perm_rel_snoc. apply IH3.
            + split; auto with supported_rel.
            + { rewrite perm_env_rel_app. rewrite perm_env_rel_one. simpl. split; [| split ].
                - rewrite perm_atom_snoc. rewrite transp_atom_thisL. reflexivity.
                - rewrite perm_rel_snoc. rewrite perm_RelCompose.
                  rewrite perm_RelSumL. rewrite perm_RelEqVal. rewrite perm_RelBot_vrel.
                  rewrite <- Hequiv1.
                  rewrite transp_rel_fresh_eq with (S := dom E'); auto with supported_rel.
                  reflexivity.
                - rewrite perm_env_rel_snoc. rewrite <- H0.
                  rewrite transp_env_rel_fresh_eq with (S := dom E'); auto with supported_rel.
                  reflexivity.
              }
            + rewrite perm_term_snoc.
              rewrite perm_close in Heqt3.
              apply close_inverse in Heqt3.
              symmetry. assumption.
        }
      × rewrite H0. rewrite <- perm_dom.
        rewrite perm_RelSumL. rewrite perm_RelEqVal. rewrite perm_RelBot_vrel.
        apply RelCompose_supported_rel; auto with supported_rel.
        apply perm_supported_rel. auto with supported_rel.
      × rewrite H0. rewrite <- perm_dom. rewrite <- perm_add.
        apply perm_supported_rel.
        apply Interp_supported with (E := (x3, RelCompose (Interp E t1 Hlc1 Hfv1) (RelSumL RelBot RelEqVal)) :: E).
        split; auto with supported_rel.
Qed.

Lemma transp_lc x y t (Hlc: lc t) : lc (transp_term x y t).
Proof.
  apply lc_equivariant. assumption.
Qed.

Lemma transp_fv_incl_dom x y E t (Hfv: fv t [<=] dom E) :
  fv (transp_term x y t) [<=] dom (transp_env_rel x y E).
Proof.
  apply (atoms_incl_equivariant x y) in Hfv.
  rewrite fv_equivariant in Hfv. rewrite dom_equivariant_rel in Hfv.
  assumption.
Qed.

Lemma Interp_equivariant E t (Hlc: lc t) (Hfv: fv t [<=] dom E) x y:
  well_supported_env E →
  RelEquiv (Interp (transp_env_rel x y E)
                   (transp_term x y t)
                   (transp_lc x y t Hlc)
                   (transp_fv_incl_dom x y E t Hfv))
           (transp_rel x y (Interp E t Hlc Hfv)).
Proof.
  intro Hsupp.
  apply (Interp_equivariant_strong E t Hlc Hfv Hsupp ((x, y) :: nil)); reflexivity.
Qed.

Lemma Interp_morphism_equiv:
  ∀ E1 E2,
    well_supported_env E1 →
    env_rel_equiv E1 E2 →
    ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E1)
      t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom E2),
      t1 = t2 →
      RelEquiv (Interp E1 t1 Hlc1 Hfv1) (Interp E2 t2 Hlc2 Hfv2).
Proof.
  intros E1 E2 Hsupp1 HequivE t1 Hlc1 Hfv1 t2 Hlc2 Hfv2 Heqt.
  symmetry.
  apply (Interp_equivariant_strong E1 t1 Hlc1 Hfv1 Hsupp1 nil E2 t2 Hlc2 Hfv2).
  - symmetry. assumption.
  - symmetry. assumption.
Qed.

Section StrongInd.

  Context (P: ∀ (E: env (rel (env term) term)) (t: term) (R: rel (env term) term), Prop)
          (HPmorphism:
             ∀ E1 E2 (HequivE: env_rel_equiv E1 E2),
             ∀ t1 t2 (Heqt: t1 = t2),
             ∀ R1 R2 (HequivR: RelEquiv R1 R2),
               P E1 t1 R1 →
               P E2 t2 R2
          )
          (HPequivariant:
             ∀ x y E t R,
               P E t R →
               P (transp_env_rel x y E) (transp_term x y t) (transp_rel x y R)
          )
          (HVar: ∀ E x (Hx: x `in` dom E)
                   (Hlc: lc (Var x))
                   (Hfv: fv (Var x) [<=] dom E)
                   R (Hget: get x E = Some R),
              P E (Var x) (RelInter (RelSelf (Var x)) (RelGather E))
          )
          (HLet: ∀ E t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
                   (Heq1: Interp E t1 Hlc1 Hfv1 = R1)
                   (IH1: P E t1 R1),
              ∀ x (Hx: x `notin` dom E) t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] add x (dom E)) R2
                (Heq2: Interp (x ¬ R1 ++ E) t2 Hlc2 Hfv2 = R2)
                (IH2: ∀ x' (Hx: x' `notin` dom E) t2' (Hlc2': lc t2') (Hfv2': fv t2' [<=] add x' (dom E)) R2'
                        (Heqt2: transp_term x x' t2 = t2')
                        (Heq2': Interp (x' ¬ R1 ++ E) t2' Hlc2' Hfv2' = R2'),
                    P (x' ¬ R1 ++ E) t2' R2'
                ),
              ∀ (Hlc: lc (Let t1 (close x t2)))
                (Hfv: fv (Let t1 (close x t2)) [<=] dom E),
                P E (Let t1 (close x t2)) (RelLet (dom E) x R1 R2)
          )
          (HLam:
             ∀ E,
             ∀ x (Hx: x `notin` dom E)
               t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] add x (dom E)) R1
               (Heq1: Interp (x ¬ RelTopEnvVal ++ E) t1 Hlc1 Hfv1 = R1)
               (IH1: ∀ x' (Hx': x' `notin` dom E) t1' (Hlc1': lc t1') (Hfv1': fv t1' [<=] add x' (dom E)) R1'
                       (Heqt1: transp_term x x' t1 = t1')
                       (Heq1': Interp (x' ¬ RelTopEnvVal ++ E) t1' Hlc1' Hfv1' = R1'),
                   P (x' ¬ RelTopEnvVal ++ E) t1' R1'),
             ∀ (Hlc: lc (Lam (close x t1)))
               (Hfv: fv (Lam (close x t1)) [<=] dom E),
               P E (Lam (close x t1))
                 (RelInter (RelLam (dom E) x RelTopEnvVal R1)
                           (RelInter (RelSelf (Lam (close x t1))) (RelGather E)))
          )
          (HApp: ∀ E,
              ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
                (Heq1: Interp E t1 Hlc1 Hfv1 = R1)
                (IH1: P E t1 R1),
              ∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom E) R2
                (Heq2: Interp E t2 Hlc2 Hfv2 = R2)
                (IH2: P E t2 R2),
              ∀ (Hlc: lc (App t1 t2))
                (Hfv: fv (App t1 t2) [<=] dom E),
                P E (App t1 t2) (APP R1 R2)
          )
          (HUnit: ∀ E (Hlc: lc Unit) (Hfv: fv Unit [<=] dom E),
              P E Unit (RelInter RelUnitR (RelGather E))
          )
          (HPair: ∀ E,
              ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
                (Heq1: Interp E t1 Hlc1 Hfv1 = R1)
                (IH1: P E t1 R1),
              ∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom E) R2
                (Heq2: Interp E t2 Hlc2 Hfv2 = R2)
                (IH2: P E t2 R2),
              ∀ (Hlc: lc (Pair t1 t2)) (Hfv: fv (Pair t1 t2) [<=] dom E),
                P E (Pair t1 t2) (RelPairR R1 R2)
          )
          (HFst: ∀ E,
              ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
                (Heq1: Interp E t1 Hlc1 Hfv1 = R1)
                (IH1: P E t1 R1),
              ∀ (Hlc: lc (Fst t1)) (Hfv: fv (Fst t1) [<=] dom E),
                P E (Fst t1) (RelCompose R1 (RelPairL RelEqVal RelTopVal))
          )
          (HSnd: ∀ E,
              ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
                (Heq1: Interp E t1 Hlc1 Hfv1 = R1)
                (IH1: P E t1 R1),
              ∀ (Hlc: lc (Snd t1)) (Hfv: fv (Snd t1) [<=] dom E),
                P E (Snd t1) (RelCompose R1 (RelPairL RelTopVal RelEqVal))
          )
          (HInjL: ∀ E,
              ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
                (Heq1: Interp E t1 Hlc1 Hfv1 = R1)
                (IH1: P E t1 R1),
              ∀ (Hlc: lc (InjL t1)) (Hfv: fv (InjL t1) [<=] dom E),
                P E (InjL t1) (RelSumR R1 RelBot)
          )
          (HInjR: ∀ E,
              ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
                (Heq1: Interp E t1 Hlc1 Hfv1 = R1)
                (IH1: P E t1 R1),
              ∀ (Hlc: lc (InjL t1)) (Hfv: fv (InjR t1) [<=] dom E),
                P E (InjR t1) (RelSumR RelBot R1)
          )
          (HMatch: ∀ E,
              ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom E) R1
                (Heq1: Interp E t1 Hlc1 Hfv1 = R1)
                (IH1: P E t1 R1),
              ∀ x2 (Hx2: x2 `notin` dom E) t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] add x2 (dom E)) R2
                (Heq2: Interp (x2 ¬ RelCompose R1 (RelSumL RelEqVal RelBot) ++ E) t2 Hlc2 Hfv2 = R2)
                (IH2: ∀ x2' (Hx2': x2' `notin` dom E) t2' (Hlc2': lc t2') (Hfv2': fv t2' [<=] add x2' (dom E)) R2'
                        (Heqt2: transp_term x2 x2' t2 = t2')
                        (Heq2': Interp (x2' ¬ RelCompose R1 (RelSumL RelEqVal RelBot) ++ E) t2' Hlc2' Hfv2' = R2'),
                    P (x2' ¬ RelCompose R1 (RelSumL RelEqVal RelBot) ++ E) t2' R2'
                ),
              ∀ x3 (Hx3: x3 `notin` dom E) t3 (Hlc3: lc t3) (Hfv3: fv t3 [<=] add x3 (dom E)) R3
                (Heq3: Interp (x3 ¬ RelCompose R1 (RelSumL RelBot RelEqVal) ++ E) t3 Hlc3 Hfv3 = R3)
                (IH3: ∀ x3' (Hx3': x3' `notin` dom E) t3' (Hlc3': lc t3') (Hfv3': fv t3' [<=] add x3' (dom E)) R3'
                        (Heqt3: transp_term x3 x3' t3 = t3')
                        (Heq3': Interp (x3' ¬ RelCompose R1 (RelSumL RelBot RelEqVal) ++ E) t3' Hlc3' Hfv3' = R3'),
                    P (x3' ¬ RelCompose R1 (RelSumL RelBot RelEqVal) ++ E) t3' R3'
                ),
              ∀ (Hlc: lc (Match t1 (close x2 t2) (close x3 t3)))
                (Hfv: fv (Match t1 (close x2 t2) (close x3 t3)) [<=] dom E),
                P E (Match t1 (close x2 t2) (close x3 t3))
                  (RelUnion
                     (RelLet (dom E) x2 (RelCompose R1 (RelSumL RelEqVal RelBot)) R2)
                     (RelLet (dom E) x3 (RelCompose R1 (RelSumL RelBot RelEqVal)) R3))
          )
  .

  Lemma Interp_strong_ind E t (Hlc: lc t) (Hfv: fv t [<=] dom E)
        (Hsupp: well_supported_env E):
    P E t (Interp E t Hlc Hfv).
  Proof.
    revert Hsupp.
    apply Interp_ind; clear E t Hlc Hfv; intros; eauto.
    - eapply HLet; eauto.
      intros x' Hx' t2' Hlc2' Hfv2' R2' Heq2' Heq. subst.
      eapply HPmorphism with
          (E1 := transp_env_rel x x' (x ¬ Interp E t1 Hlc1 Hfv1 ++ E))
          (t1 := transp_term x x' t2)
          (R1 := transp_rel x x' (Interp (x ¬ Interp E t1 Hlc1 Hfv1 ++ E) t2 Hlc2 Hfv2)).
      + rewrite transp_env_rel_app. rewrite transp_env_rel_one.
        rewrite transp_atom_thisL. simpl; split; [ reflexivity | split ].
        × apply transp_rel_fresh_eq with (S := dom E); auto with supported_rel.
        × apply transp_env_rel_fresh_eq with (S := dom E); auto with supported_rel.
      + reflexivity.
      + rewrite <- Interp_equivariant.
        × { apply Interp_morphism_equiv.
            - apply well_supported_env_equivariant. simpl. auto with supported_rel.
            - simpl. split; [| split].
              + apply transp_atom_thisL.
              + apply transp_rel_fresh_eq with (S := dom E); auto with supported_rel.
              + apply transp_env_rel_fresh_eq with (S := dom E); auto.
            - reflexivity.
          }
        × simpl. auto with supported_rel.
      + apply HPequivariant.
        apply IH2. simpl; auto with supported_rel.
    - eapply HLam; eauto.
      intros x' Hx' t1' Hlc1' Hfv1' R1' Heq1' Heq. subst.
      eapply HPmorphism with
          (E1 := transp_env_rel x x' (x ¬ RelTopEnvVal ++ E))
          (t1 := transp_term x x' t1)
          (R1 := transp_rel x x' (Interp (x ¬ RelTopEnvVal ++ E) t1 Hlc1 Hfv1)).
      + rewrite transp_env_rel_app. rewrite transp_env_rel_one.
        rewrite transp_atom_thisL. simpl; split; [ reflexivity | split ].
        × apply RelTopEnvVal_rel_equivariant.
        × apply transp_env_rel_fresh_eq with (S := dom E); auto.
      + reflexivity.
      + rewrite <- Interp_equivariant.
        × { apply Interp_morphism_equiv.
            - apply well_supported_env_equivariant. simpl. auto with supported_rel.
            - simpl. split; [| split].
              + apply transp_atom_thisL.
              + apply RelTopEnvVal_rel_equivariant.
              + apply transp_env_rel_fresh_eq with (S := dom E); auto.
            - reflexivity.
          }
        × simpl. auto with supported_rel.
      + apply HPequivariant.
        apply IH1. simpl; auto with supported_rel.
    - eapply HMatch; eauto.
      + intros x2' Hx2' t2' Hlc2' Hfv2' R2' Heq2' Heq. subst.
        eapply HPmorphism with
            (E1 := transp_env_rel x2 x2' (x2 ¬ RelCompose (Interp E t1 Hlc1 Hfv1) (RelSumL RelEqVal RelBot) ++ E))
            (t1 := transp_term x2 x2' t2)
            (R1 := transp_rel x2 x2' (Interp (x2 ¬ RelCompose (Interp E t1 Hlc1 Hfv1) (RelSumL RelEqVal RelBot) ++ E) t2 Hlc2 Hfv2)).
        × { rewrite transp_env_rel_app. rewrite transp_env_rel_one.
            rewrite transp_atom_thisL. simpl; split; [ reflexivity | split ].
            × apply transp_rel_fresh_eq with (S := dom E); auto with supported_rel.
            × apply transp_env_rel_fresh_eq with (S := dom E); auto with supported_rel.
          }
        × reflexivity.
        × { rewrite <- Interp_equivariant.
            - apply Interp_morphism_equiv.
              + apply well_supported_env_equivariant. simpl. auto with supported_rel.
              + simpl. split; [| split].
                × apply transp_atom_thisL.
                × apply transp_rel_fresh_eq with (S := dom E); auto with supported_rel.
                × apply transp_env_rel_fresh_eq with (S := dom E); auto.
              + reflexivity.
            - simpl. auto with supported_rel.
          }
        × apply HPequivariant.
          apply IH2. simpl; auto with supported_rel.
      + intros x3' Hx3' t3' Hlc3' Hfv3' R3' Heq3' Heq. subst.
        eapply HPmorphism with
            (E1 := transp_env_rel x3 x3' (x3 ¬ RelCompose (Interp E t1 Hlc1 Hfv1) (RelSumL RelBot RelEqVal) ++ E))
            (t1 := transp_term x3 x3' t3)
            (R1 := transp_rel x3 x3' (Interp (x3 ¬ RelCompose (Interp E t1 Hlc1 Hfv1) (RelSumL RelBot RelEqVal) ++ E) t3 Hlc3 Hfv3)).
        × { rewrite transp_env_rel_app. rewrite transp_env_rel_one.
            rewrite transp_atom_thisL. simpl; split; [ reflexivity | split ].
            × apply transp_rel_fresh_eq with (S := dom E); auto with supported_rel.
            × apply transp_env_rel_fresh_eq with (S := dom E); auto with supported_rel.
          }
        × reflexivity.
        × { rewrite <- Interp_equivariant.
            - apply Interp_morphism_equiv.
              + apply well_supported_env_equivariant. simpl. auto with supported_rel.
              + simpl. split; [| split].
                × apply transp_atom_thisL.
                × apply transp_rel_fresh_eq with (S := dom E); auto with supported_rel.
                × apply transp_env_rel_fresh_eq with (S := dom E); auto.
              + reflexivity.
            - simpl. auto with supported_rel.
          }
        × apply HPequivariant.
          apply IH3. simpl; auto with supported_rel.
  Qed.
End StrongInd.

Lemma Interp_sub_strong E1 E2 t (Hlc1: lc t) (Hfv1: fv t [<=] dom E1)
      (Hlc2: lc t) (Hfv2: fv t [<=] dom E2):
  uniq E1 →
  wf_env_rel E1 →
  wf_env_rel E2 →
  env_rel_incl E1 E2 →
  RelIncl (Interp E1 t Hlc1 Hfv1) (Interp E2 t Hlc2 Hfv2).
Proof.
  intros Huniq Hwf Hwf2 Hincl.
  assert (well_supported_env E1) as Hsupp by auto.
  revert Huniq Hwf E2 Hlc2 Hfv2 Hwf2 Hincl.
  apply Interp_strong_ind with
      (P := fun E1 t a ⇒
              ∀ (Huniq1: uniq E1)
                (Hwf1: wf_env_rel E1),
              ∀ E2 (Hlc2: lc t) (Hfv2 : fv t [<=] dom E2)
                (Hwf2: wf_env_rel E2)
                (Hincl: env_rel_incl E1 E2),
                RelIncl a (Interp E2 t Hlc2 Hfv2)
      ); auto; try clear E1 t Hlc1 Hfv1; intros.
  - subst t2. rewrite <- H; auto.
    + rewrite HequivE. assumption.
    + rewrite HequivE. assumption.
    + rewrite <- Hincl. apply env_rel_incl_refl_equiv. assumption.
  - apply (RelIncl_rel_equivariant x y).
    rewrite transp_rel_involution.
    rewrite <- Interp_equivariant; auto.
    erewrite Interp_proof_irrelevant
      with (E2 := transp_env_rel x y E2) (t2 := t0).
    + apply H.
      × apply uniq_rel_equivariant in Huniq1. assumption.
      × apply wf_env_rel_equivariant in Hwf1. assumption.
      × apply wf_env_rel_equivariant. assumption.
      × apply (env_rel_incl_equivariant x y). rewrite transp_env_rel_involution.
        assumption.
    + reflexivity.
    + apply transp_term_involution.
      Unshelve.
      × apply lc_equivariant in Hlc2. assumption.
      × apply (transp_fv_incl_dom x y) in Hfv2.
        rewrite transp_term_involution in Hfv2.
        assumption.
  - destruct (Interp_equations E2 (Var x) Hlc2 Hfv2) as [y [Hgety Heq]].
    rewrite Heq. clear Heq.
    rewrite Hincl. reflexivity.
  - destruct (Interp_equations E2 (Let t1 (close x t2)) Hlc3 Hfv3) as
        [y [Hy [t2' [Heqt2 [Hlc1' [Hfv1' [Hlc2' [Hfv2' Heq]]]]]]]].
    rewrite Heq. clear Heq.
    simpl.
    apply close_inverse in Heqt2.
    assert (dom E [=] dom E2) as Heqdom by auto using env_rel_incl_dom.
    rewrite <- Heqdom in Hy.
    rewrite <- Heqdom.
    assert (supported_rel (dom E) R1) as Hsupp1.
    { rewrite <- Heq1. simpl. auto with supported_rel. }
    assert (wf_env_rel ([(x, R1)] ++ E)) as Hwf1'.
    { rewrite <- Heq1. auto with wf_rel. }
    assert (supported_rel (add x (dom E)) R2) as Hsupp2.
    { rewrite <- Heq2. apply Interp_supported with (E := x ¬ R1 ++ E). auto. }
    rewrite (RelLet_bound_var_rename _ x y); auto.
    apply RelLet_morphism_incl; auto; try reflexivity.
    rewrite <- Heq2.
    rewrite <- Interp_equivariant; auto.
    erewrite Interp_morphism_equiv with (E2 := y ¬ R1 ++ E) (t2 := t2'); auto.
    + eapply IH2 with (x' := y); eauto.
      × simpl_env. auto with wf_rel.
      × simpl. auto.
    + apply well_supported_env_equivariant. auto.
    + rewrite transp_env_rel_app. rewrite transp_env_rel_one.
      rewrite transp_atom_thisL. simpl. split; [ reflexivity | split ].
      × apply transp_rel_fresh_eq with (S := dom E); auto.
      × apply transp_env_rel_fresh_eq with (S := dom E); auto.
      Unshelve.
      -- assumption.
      -- rewrite Heqdom. assumption.
  - destruct (Interp_equations E2 (Lam (close x t1)) Hlc2 Hfv2) as
        [y [Hy [t1' [Heqt1 [Hlc1' [Hfv1' Heq]]]]]].
    rewrite Heq. clear Heq.
    simpl.
    assert (dom E [=] dom E2) as Heqdom by auto using env_rel_incl_dom.
    rewrite <- Heqdom in Hy.
    rewrite <- Heqdom.
    assert (wf_env_rel ([(x, RelTopEnvVal)] ++ E)) as Hwf1' by auto with wf_rel.
    assert (supported_rel (add x (dom E)) R1) as Hsupp2.
    { rewrite <- Heq1. apply Interp_supported with (E := x ¬ RelTopEnvVal ++ E). auto. }
    rewrite (RelLam_bound_var_rename _ x y); auto with good_rel supported_rel.
    rewrite Heqt1.
    rewrite (RelGather_morphism_incl _ _ Hincl).
    apply RelInter_morphism_incl; [| reflexivity].
    apply RelLam_incl; auto; try reflexivity.
    rewrite <- Heq1.
    apply close_inverse in Heqt1.
    rewrite <- Interp_equivariant; auto.
    erewrite Interp_morphism_equiv with (E2 := y ¬ RelTopEnvVal ++ E) (t2 := t1'); auto.
    + eapply IH1 with (x' := y); eauto.
      × simpl_env. auto with wf_rel.
      × simpl. split; [| split]; auto. reflexivity.
    + apply well_supported_env_equivariant. auto.
    + rewrite transp_env_rel_app. rewrite transp_env_rel_one.
      rewrite transp_atom_thisL. simpl. split; [ reflexivity | split ].
      × apply transp_rel_fresh_eq with (S := dom E); auto with supported_rel.
      × apply transp_env_rel_fresh_eq with (S := dom E); auto.
      Unshelve.
      -- assumption.
      -- rewrite Heqdom. assumption.
  - destruct (Interp_equations E2 (App t1 t2) Hlc3 Hfv3) as
        [Hlc1' [Hfv1' [Hlc2' [Hfv2' Heq]]]].
    rewrite Heq. clear Heq.
    simpl. apply APP_morphism_incl; auto.
  - rewrite (Interp_equations E2 Unit Hlc2 Hfv2).
    rewrite (RelGather_morphism_incl _ _ Hincl).
    reflexivity.
  - destruct (Interp_equations E2 (Pair t1 t2) Hlc3 Hfv3) as
        [Hlc1' [Hfv1' [Hlc2' [Hfv2' Heq]]]].
    rewrite Heq. clear Heq.
    simpl. apply RelPairR_morphism_incl; auto.
  - destruct (Interp_equations E2 (Fst t1) Hlc2 Hfv2) as [Hlc1' [Hfv1' Heq]].
    rewrite Heq. clear Heq.
    simpl. apply RelCompose_morphism_incl; auto. reflexivity.
  - destruct (Interp_equations E2 (Snd t1) Hlc2 Hfv2) as [Hlc1' [Hfv1' Heq]].
    rewrite Heq. clear Heq.
    simpl. apply RelCompose_morphism_incl; auto. reflexivity.
  - destruct (Interp_equations E2 (InjL t1) Hlc2 Hfv2) as [Hlc1' [Hfv1' Heq]].
    rewrite Heq. clear Heq.
    simpl. apply RelSumR_morphism_incl; auto. reflexivity.
  - destruct (Interp_equations E2 (InjR t1) Hlc2 Hfv2) as [Hlc1' [Hfv1' Heq]].
    rewrite Heq. clear Heq.
    simpl. apply RelSumR_morphism_incl; auto. reflexivity.
  - destruct (Interp_equations E2 (Match t1 (close x2 t2) (close x3 t3)) Hlc4 Hfv4) as
        [y2 [Hy2 [t2' [Heqt2 [y3 [Hy3 [t3' [Heqt3 [Hlc1' [Hfv1' [Hlc2' [Hfv2' [Hlc3' [Hfv3' Heq]]]]]]]]]]]]]].
    rewrite Heq. clear Heq.
    simpl.
    assert (dom E [=] dom E2) as Heqdom by auto using env_rel_incl_dom.
    rewrite <- Heqdom in Hy2.
    rewrite <- Heqdom in Hy3.
    rewrite <- Heqdom.
    apply RelUnion_morphism_incl.
    + assert (supported_rel (dom E) (RelCompose R1 (RelSumL RelEqVal RelBot))) as Hsupp1'.
      { rewrite <- Heq1. simpl. auto with supported_rel. }
      assert (wf_env_rel ([(x2, RelCompose R1 (RelSumL RelEqVal RelBot))] ++ E)) as Hwf1'.
      { rewrite <- Heq1. auto with wf_rel. }
      assert (supported_rel (add x2 (dom E)) R2) as Hsupp2'.
      { rewrite <- Heq2. apply Interp_supported with (E := x2 ¬ RelCompose R1 (RelSumL RelEqVal RelBot) ++ E). auto. }
      rewrite (RelLet_bound_var_rename _ x2 y2); auto.
      apply RelLet_morphism_incl; auto; try reflexivity.
      × rewrite IH1; try reflexivity; auto.
      × { rewrite <- Heq2.
          apply close_inverse in Heqt2.
          rewrite <- Interp_equivariant; auto.
          erewrite Interp_morphism_equiv with (E2 := y2 ¬ RelCompose R1 (RelSumL RelEqVal RelBot) ++ E) (t2 := t2'); auto.
          - eapply IH2 with (x2' := y2); eauto.
            + simpl_env. auto with wf_rel.
            + simpl. split; [| split]; auto.
              rewrite IH1; try reflexivity; auto.
          - apply well_supported_env_equivariant. auto.
          - rewrite transp_env_rel_app. rewrite transp_env_rel_one.
            rewrite transp_atom_thisL. simpl. split; [ reflexivity | split ].
            + apply transp_rel_fresh_eq with (S := dom E); auto.
            + apply transp_env_rel_fresh_eq with (S := dom E); auto.
            Unshelve.
            × assumption.
            × rewrite Heqdom. assumption.
        }
    + assert (supported_rel (dom E) (RelCompose R1 (RelSumL RelBot RelEqVal))) as Hsupp1'.
      { rewrite <- Heq1. simpl. auto with supported_rel. }
      assert (wf_env_rel ([(x2, RelCompose R1 (RelSumL RelBot RelEqVal))] ++ E)) as Hwf1'.
      { rewrite <- Heq1. auto with wf_rel. }
      assert (supported_rel (add x3 (dom E)) R3) as Hsupp3'.
      { rewrite <- Heq3. apply Interp_supported with (E := x3 ¬ RelCompose R1 (RelSumL RelBot RelEqVal) ++ E). auto. }
      rewrite (RelLet_bound_var_rename _ x3 y3); auto.
      apply RelLet_morphism_incl; auto; try reflexivity.
      × rewrite IH1; try reflexivity; auto.
      × { rewrite <- Heq3.
          apply close_inverse in Heqt3.
          rewrite <- Interp_equivariant; auto.
          erewrite Interp_morphism_equiv with (E2 := y3 ¬ RelCompose R1 (RelSumL RelBot RelEqVal) ++ E) (t2 := t3'); auto.
          - eapply IH3 with (x3' := y3); eauto.
            + simpl_env. auto with wf_rel.
            + simpl. split; [| split]; auto.
              rewrite IH1; try reflexivity; auto.
          - apply well_supported_env_equivariant. auto.
          - rewrite transp_env_rel_app. rewrite transp_env_rel_one.
            rewrite transp_atom_thisL. simpl. split; [ reflexivity | split ].
            + apply transp_rel_fresh_eq with (S := dom E); auto.
            + apply transp_env_rel_fresh_eq with (S := dom E); auto.
            Unshelve.
            × assumption.
            × rewrite Heqdom. assumption.
        }
Qed.

Lemma Interp_monotonic E1 E2 t (Hlc: lc t) (Hfv1: fv t [<=] dom E1) (Hfv2: fv t [<=] dom E2):
  uniq E1 →
  wf_env_rel E1 →
  wf_env_rel E2 →
  env_rel_incl E1 E2 →
  RelIncl (Interp E1 t Hlc Hfv1) (Interp E2 t Hlc Hfv2).
Proof.
  intros. apply Interp_sub_strong; auto.
Qed.

Lemma Interp_functional_monotonic E x t (Hlc: lc t) (Hfv: fv t [<=] add x (dom E)):
  x `notin` dom E →
  uniq E →
  wf_env_rel E →
  ∀ R1, wf_rel (dom E) R1 →
        ∀ R2, wf_rel (dom E) R2 →
              RelIncl R1 R2 →
              RelIncl (Interp (x ¬ R1 ++ E) t Hlc Hfv) (Interp (x ¬ R2 ++ E) t Hlc Hfv).
Proof.
  intros Hx Huniq HwfE R1 Hwf1 R2 Hwf2 Hincl.
  apply Interp_monotonic; auto with wf_rel.
  simpl. split; [| split]; auto.
  reflexivity.
Qed.