Coral.RLogicStrong: strong version of RLogic, that provides stronger induction principles

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 RelWf.
Require Import RLogic.

Inductive RLogic_strong : env (rel (env term) term) → term → rel (env term) term → Prop :=
| RLogicEquiv_strong: ∀ E t R1 R2,
    RelEquiv R1 R2 →
    RLogic_strong E t R1 →
    RLogic_strong E t R2
| RLogicInter_strong: ∀ E t R1 R2,
    RLogic_strong E t R1 →
    RLogic_strong E t R2 →
    RLogic_strong E t (RelInter R1 R2)
| RLogicSub_strong: ∀ E t R1 R2,
    wf_rel (dom E) R2 →
    RLogic_strong E t R1 →
    RelIncl R1 R2 →
    RLogic_strong E t R2
| RLogicSelf_strong: ∀ E t R,
    RLogic_strong E t R →
    is_extended_value t →
    RLogic_strong E t (RelSelf t)
| RLogicGather_strong: ∀ E t R,
    RLogic_strong E t R →
    RLogic_strong E t (RelGather E)
| RLogicVar_strong: ∀ E x R,
    get x E = Some R →
    RLogic_strong E (Var x) R
| RLogicLet_strong: ∀ E t1 t2 R1 R2,
    ∀ (Hparametric: parametric_family_rel (dom E) R2),
      RLogic_strong E t1 R1 →
      (∀ x, x `notin` dom E → RLogic_strong (x ¬ R1 ++ E) (t2 ^ x) (R2 x)) →
      RLogic_strong E (Let t1 t2) (RelLet_strong (dom E) R2 R1)
| RLogicLam_strong:
    ∀ E t R1 R2
      (Hparametric: parametric_family_rel (dom E) R2)
      (Hwf: wf_rel (dom E) R1),
      (∀ x, x `notin` dom E → RLogic_strong (x ¬ R1 ++ E) (t ^ x) (R2 x)) →
      RLogic_strong E (Lam t) (RelLam_strong (dom E) R1 R2)
| RLogicApp_strong: ∀ E t1 t2 R1 R2,
    RLogic_strong E t1 R1 →
    RLogic_strong E t2 R2 →
    RLogic_strong E (App t1 t2) (APP R1 R2)
| RLogicUnit_strong: ∀ E,
    RLogic_strong E Unit RelUnitR
| RLogicPair_strong: ∀ E t1 t2 R1 R2,
    RLogic_strong E t1 R1 →
    RLogic_strong E t2 R2 →
    RLogic_strong E (Pair t1 t2) (RelPairR R1 R2)
| RLogicFst_strong: ∀ E t R,
    RLogic_strong E t R →
    RLogic_strong E (Fst t) (RelCompose R (RelPairL RelEqVal RelTopVal))
| RLogicSnd_strong: ∀ E t R,
    RLogic_strong E t R →
    RLogic_strong E (Snd t) (RelCompose R (RelPairL RelTopVal RelEqVal))
| RLogicInjL_strong: ∀ E t R,
    RLogic_strong E t R →
    RLogic_strong E (InjL t) (RelSumR R RelBot)
| RLogicInjR_strong: ∀ E t R,
    RLogic_strong E t R →
    RLogic_strong E (InjR t) (RelSumR RelBot R)
| RLogicMatch_strong: ∀ E t t1 t2 R R1 R2,
    ∀ (Hparametric1: parametric_family_rel (dom E) R1)
      (Hparametric2: parametric_family_rel (dom E) R2),
      RLogic_strong E t R →
      (∀ x1, x1 `notin` dom E →
             RLogic_strong (x1 ¬ (RelCompose R (RelSumL RelEqVal RelBot)) ++ E) (t1 ^ x1) (R1 x1)) →
      (∀ x2, x2 `notin` dom E →
             RLogic_strong (x2 ¬ (RelCompose R (RelSumL RelBot RelEqVal)) ++ E) (t2 ^ x2) (R2 x2)) →
      RLogic_strong E (Match t t1 t2)
                    (RelUnion
                       (RelLet_strong (dom E) R1 (RelCompose R (RelSumL RelEqVal RelBot)))
                       (RelLet_strong (dom E) R2 (RelCompose R (RelSumL RelBot RelEqVal)))
                    )
.

Add Parametric Morphism: RLogic_strong
    with signature env_rel_equiv ==> eq ==> RelEquiv ==> iff
      as RLogic_strong_morphism_equiv.
Proof.
  assert (∀ E1 E2 t R,
             env_rel_equiv E1 E2 →
             RLogic_strong E1 t R →
             RLogic_strong E2 t R).
  { intros E1 E2 t R H12 H.
    generalize dependent E2.
    induction H; intros.
    - eapply RLogicEquiv_strong; eauto.
    - apply RLogicInter_strong; auto.
    - eapply RLogicSub_strong; eauto. rewrite <- H12. assumption.
    - eapply RLogicSelf_strong; eauto.
    - apply RLogicEquiv_strong with (R1 := RelGather E2).
      + rewrite H12. reflexivity.
      + eapply RLogicGather_strong; eauto.
    - case_eq (get x E2); intros.
      + eapply env_rel_equiv_get in H; [| symmetry |]; eauto.
        eapply RLogicEquiv_strong with (R1 := r); auto.
        apply RLogicVar_strong; auto.
      + exfalso. rewrite <- env_rel_equiv_get_None in H0; eauto. congruence.
    - apply RLogicEquiv_strong with (R1 := RelLet_strong (dom E2) R2 R1).
      + rewrite H12. reflexivity.
      + apply RLogicLet_strong; auto.
        × rewrite <- H12. assumption.
        × { intros x Hx. apply H1.
            - rewrite H12. assumption.
            - simpl; split; [| split]; auto. reflexivity.
          }
    - eapply RLogicEquiv_strong with (R1 := RelLam_strong (dom E2) R1 R2).
      + rewrite H12. reflexivity.
      + apply RLogicLam_strong; auto.
        × rewrite <- H12. assumption.
        × rewrite <- H12. assumption.
        × { intros x Hx. apply H0.
            - rewrite H12. assumption.
            - simpl; split; [| split]; auto. reflexivity.
          }
    - apply RLogicApp_strong; auto.
    - apply RLogicUnit_strong; auto.
    - apply RLogicPair_strong; auto.
    - apply RLogicFst_strong; auto.
    - apply RLogicSnd_strong; auto.
    - apply RLogicInjL_strong; auto.
    - apply RLogicInjR_strong; auto.
    - apply RLogicEquiv_strong with
          (R1 := RelUnion
                   (RelLet_strong (dom E2) R1 (RelCompose R (RelSumL RelEqVal RelBot)))
                   (RelLet_strong (dom E2) R2 (RelCompose R (RelSumL RelBot RelEqVal)))
          ).
      + rewrite H12. reflexivity.
      + apply RLogicMatch_strong; auto.
        × rewrite <- H12. assumption.
        × rewrite <- H12. assumption.
        × { intros x Hx. apply H1.
            - rewrite H12. assumption.
            - simpl; split; [| split]; auto. reflexivity.
          }
        × { intros x Hx. apply H3.
            - rewrite H12. assumption.
            - simpl; split; [| split]; auto. reflexivity.
          }
  }
  intros E1 E2 HE t R1 R2 HR.
  split; intro HRLogic.
  - eapply RLogicEquiv_strong; eauto.
  - symmetry in HR. symmetry in HE. eapply RLogicEquiv_strong; eauto.
Qed.

Lemma RLogic_strong_equivariant x y E t R:
  RLogic_strong E t R →
  RLogic_strong (transp_env_rel x y E) (transp_term x y t) (transp_rel x y R).
Proof.
  intro H. induction H; simpl.
  - eapply RLogicEquiv_strong; eauto. rewrite H. reflexivity.
  - rewrite RelInter_rel_equivariant.
    apply RLogicInter_strong; auto.
  - apply (RelIncl_rel_equivariant x y) in H1.
    rewrite (wf_rel_equivariant x y) in H.
    rewrite dom_equivariant_rel in H.
    eapply RLogicSub_strong; eauto.
  - rewrite RelSelf_rel_equivariant.
    rewrite <- (is_extended_value_equivariant x y) in H0.
    eapply RLogicSelf_strong; eauto.
  - rewrite RelGather_rel_equivariant.
    eapply RLogicGather_strong; eauto.
  - apply RLogicVar_strong with (R := transp_rel x y R).
    apply get_transp_env_rel_Some_equivariant. assumption.
  - rewrite RelLet_strong_rel_equivariant.
    apply (parametric_family_rel_equivariant x y) in Hparametric.
    rewrite dom_equivariant_rel in Hparametric.
    rewrite dom_equivariant_rel.
    apply RLogicLet_strong; auto.
    intros z Hz.
    apply (notin_equivariant x y) in Hz.
    rewrite dom_equivariant_rel in Hz.
    rewrite transp_env_rel_involution in Hz.
    specialize (H1 (transp_atom x y z) Hz).
    unfold transp_env_rel in H1.
    rewrite open_equivariant in H1.
    simpl in H1.
    rewrite transp_atom_involution in H1.
    assumption.
  - rewrite RelLam_strong_equivariant.
    rewrite dom_equivariant_rel.
    eapply RLogicLam_strong; eauto.
    + rewrite <- dom_equivariant_rel.
      apply parametric_family_rel_equivariant.
      assumption.
    + rewrite <- dom_equivariant_rel.
      apply wf_rel_equivariant.
      assumption.
    + intros z Hz.
      apply (notin_equivariant x y) in Hz.
      rewrite dom_equivariant_rel in Hz.
      rewrite transp_env_rel_involution in Hz.
      specialize (H0 (transp_atom x y z) Hz).
      rewrite transp_env_rel_app in H0.
      rewrite transp_env_rel_one in H0.
      rewrite open_equivariant in H0.
      simpl in H0.
      rewrite transp_atom_involution in H0.
      assumption.
  - rewrite APP_rel_equivariant.
    apply RLogicApp_strong; auto.
  - rewrite RelUnitR_rel_equivariant.
    apply RLogicUnit_strong.
  - rewrite RelPairR_rel_equivariant.
    apply RLogicPair_strong; auto.
  - rewrite RelCompose_rel_equivariant.
    rewrite RelPairL_vrel_equivariant.
    rewrite RelTopVal_vrel_equivariant.
    rewrite RelEqVal_vrel_equivariant.
    apply RLogicFst_strong; auto.
  - rewrite RelCompose_rel_equivariant.
    rewrite RelPairL_vrel_equivariant.
    rewrite RelTopVal_vrel_equivariant.
    rewrite RelEqVal_vrel_equivariant.
    apply RLogicSnd_strong; auto.
  - rewrite RelSumR_rel_equivariant.
    rewrite RelBot_rel_equivariant.
    apply RLogicInjL_strong; auto.
  - rewrite RelSumR_rel_equivariant.
    rewrite RelBot_rel_equivariant.
    apply RLogicInjR_strong; auto.
  - rewrite RelUnion_rel_equivariant.
    repeat rewrite RelLet_strong_rel_equivariant.
    repeat rewrite RelCompose_rel_equivariant.
    repeat rewrite RelSumL_vrel_equivariant.
    repeat rewrite RelBot_vrel_equivariant.
    repeat rewrite RelTopVal_vrel_equivariant.
    repeat rewrite RelEqVal_vrel_equivariant.
    repeat rewrite dom_equivariant_rel.
    apply (parametric_family_rel_equivariant x y) in Hparametric1.
    rewrite dom_equivariant_rel in Hparametric1.
    apply (parametric_family_rel_equivariant x y) in Hparametric2.
    rewrite dom_equivariant_rel in Hparametric2.
    apply RLogicMatch_strong; auto.
    + intros z Hz.
      apply (notin_equivariant x y) in Hz.
      rewrite dom_equivariant_rel in Hz.
      rewrite transp_env_rel_involution in Hz.
      specialize (H1 (transp_atom x y z) Hz).
      unfold transp_env_rel in H1.
      rewrite open_equivariant in H1.
      simpl in H1. simpl_env in H1.
      rewrite transp_atom_involution in H1.
      assert (env_rel_equiv
                [(z, transp_rel x y (RelCompose R (RelSumL RelEqVal RelBot)))]
                [(z, RelCompose (transp_rel x y R) (RelSumL RelEqVal RelBot))]) as Heq.
      { simpl; split; [| split]; auto.
        rewrite RelCompose_rel_equivariant.
        rewrite RelSumL_vrel_equivariant.
        rewrite RelEqVal_vrel_equivariant.
        rewrite RelBot_vrel_equivariant.
        reflexivity.
      }
      rewrite Heq in H1.
      assumption.
    + intros z Hz.
      apply (notin_equivariant x y) in Hz.
      rewrite dom_equivariant_rel in Hz.
      rewrite transp_env_rel_involution in Hz.
      specialize (H3 (transp_atom x y z) Hz).
      unfold transp_env_rel in H3.
      rewrite open_equivariant in H3.
      simpl in H3. simpl_env in H3.
      rewrite transp_atom_involution in H3.
      assert (env_rel_equiv
                [(z, transp_rel x y (RelCompose R (RelSumL RelBot RelEqVal)))]
                [(z, RelCompose (transp_rel x y R) (RelSumL RelBot RelEqVal))]) as Heq.
      { simpl; split; [| split]; auto.
        rewrite RelCompose_rel_equivariant.
        rewrite RelSumL_vrel_equivariant.
        rewrite RelEqVal_vrel_equivariant.
        rewrite RelBot_vrel_equivariant.
        reflexivity.
      }
      rewrite Heq in H3.
      assumption.
Qed.

Lemma RLogic_strong_lc E t R:
  RLogic_strong E t R →
  lc t.
Proof.
  intro H. induction H; auto with lngen.
  - pick fresh x for (dom E).
    eapply lc_Let_exists; eauto.
  - pick fresh x for (dom E).
    eapply lc_Lam_exists; eauto.
  - pick fresh x for (dom E).
    eapply lc_Match_exists; eauto.
Qed.

Lemma RLogic_strong_fv E t R:
  RLogic_strong E t R →
  fv t [<=] dom E.
Proof.
  intro H; induction H; simpl; try fsetdec.
  - apply get_in_dom in H. fsetdec.
  - assert (fv t2 [<=] dom E).
    { pick fresh x for (fv t2 `union` dom E).
      specialize (H1 x). rewrite dom_app in H1. rewrite dom_one in H1.
      assert (fv t2 [<=] singleton x `union` dom E).
      { rewrite <- H1; auto with lngen. }
      fsetdec.
    }
    fsetdec.
  - pick fresh x for (fv t `union` dom E).
    specialize (H0 x). rewrite dom_app in H0. rewrite dom_one in H0.
    assert (fv t [<=] singleton x `union` dom E).
    { rewrite <- H0; auto with lngen. }
    fsetdec.
  - assert (fv t1 [<=] dom E).
    { pick fresh x for (fv t1 `union` dom E).
      specialize (H1 x). rewrite dom_app in H1. rewrite dom_one in H1.
      assert (fv t1 [<=] singleton x `union` dom E).
      { rewrite <- H1; auto with lngen. }
      fsetdec.
    }
    assert (fv t2 [<=] dom E).
    { pick fresh x for (fv t2 `union` dom E).
      specialize (H3 x). rewrite dom_app in H3. rewrite dom_one in H3.
      assert (fv t2 [<=] singleton x `union` dom E).
      { rewrite <- H3; auto with lngen. }
      fsetdec.
    }
    fsetdec.
Qed.

Lemma RLogic_strong_supported E t R:
  well_supported_env E →
  RLogic_strong E t R →
  supported_rel (dom E) R.
Proof.
  intros HEsupp HRLogic. induction HRLogic.
  - rewrite <- H. auto.
  - apply RelInter_supported_rel; auto.
  - auto.
  - apply (supported_rel_subset (fv t)); eauto.
    + eapply RLogic_strong_fv; eauto.
    + apply RelSelf_supported_rel.
  - apply RelGather_supported_rel. auto.
  - eapply supported_env_rel_get; eauto.
  - apply RelLet_strong_supported_rel; auto; try reflexivity.
    apply supported_family_rel_intro; auto.
    intros x Hx. apply (H0 x Hx); auto.
    simpl. split; auto.
  - apply RelLam_strong_supported; eauto.
    apply supported_family_rel_intro; auto.
    intros x Hx. apply (H0 x Hx); auto.
    simpl. split; auto with supported_rel.
  - apply APP_supported_rel.
    + apply IHHRLogic1; auto.
    + apply IHHRLogic2; auto.
  - auto with supported_rel.
  - apply RelPairR_supported_rel.
    + apply IHHRLogic1; auto.
    + apply IHHRLogic2; auto.
  - auto 7 with supported_rel.
  - auto 7 with supported_rel.
  - auto with supported_rel.
  - auto with supported_rel.
  - assert (supported_rel (dom E) R).
    { apply IHHRLogic; auto. }
    apply RelUnion_supported_rel.
    + apply RelLet_strong_supported_rel; auto with supported_rel.
      apply supported_family_rel_intro; auto.
      intros x Hx. apply (H0 x Hx); auto.
      simpl.
      split; auto with supported_rel.
    + apply RelLet_strong_supported_rel; auto with supported_rel.
      apply supported_family_rel_intro; auto.
      intros x Hx. apply (H2 x Hx); auto.
      simpl.
      split; auto with supported_rel.
Qed.
Hint Resolve RLogic_strong_supported: supported_rel.

Lemma RLogic_strong_rename y x Rx E t R:
  well_supported_env (x ¬ Rx ++ E) →
  x `notin` dom E →
  y `notin` dom E →
  RLogic_strong (x ¬ Rx ++ E) t R →
  RLogic_strong (y ¬ Rx ++ E) (subst (Var y) x t) (transp_rel y x R).
Proof.
  intros HE Hx Hy H.
  simpl in HE. destruct HE as [HR HE].
  assert (fv t [<=] add x (dom E)) as Hfv.
  { apply RLogic_strong_fv in H. assumption. }
  apply (RLogic_strong_equivariant y x) in H.
  rewrite transp_env_rel_app in H.
  assert (env_rel_equiv (transp_env_rel y x (x ¬ Rx)) (y ¬ Rx)) as Heq.
  { simpl. split; [| split]; auto using transp_atom_thisR. }
  rewrite Heq in H.
  rewrite transp_env_rel_fresh_eq in H; auto.
  destruct (y == x); subst.
  - rewrite transp_term_refl in H.
    rewrite subst_refl. assumption.
  - rewrite transp_term_freshL_is_subst in H; auto. fsetdec.
Qed.

Lemma RLogicLet_exists E t1 x t2 R1 R2:
  well_supported_env (x ¬ R1 ++ E) →
  RLogic_strong E t1 R1 →
  x `notin` dom E →
  RLogic_strong (x ¬ R1 ++ E) t2 R2 →
  RLogic_strong E (Let t1 (close x t2)) (RelLet_strong (dom E) (lambda_rel x R2) R1).
Proof.
  intros HsuppE H1 Hx H2.
  apply RLogicLet_strong; auto.
  - apply parametric_family_rel_lambda_rel.
    apply (supported_rel_subset (dom (x ¬ R1 ++ E))); [reflexivity|].
    eapply RLogic_strong_supported; eauto.
  - intros y Hy.
    apply (RLogic_strong_rename y x) in H2; auto.
    unfold lambda_rel.
    rewrite (subst_intro x).
    + rewrite open_close. assumption.
    + rewrite fv_close. auto.
Qed.

Lemma RLogicLam_exists E x t R1 R2:
  well_supported_env E →
  wf_rel (dom E) R1 →
  x `notin` dom E →
  RLogic_strong (x ¬ R1 ++ E) t R2 →
  RLogic_strong E (Lam (close x t)) (RelLam_strong (dom E) R1 (lambda_rel x R2)).
Proof.
  intros HsuppE Hwf Hx H2.
  apply RLogicLam_strong; auto.
  - apply parametric_family_rel_lambda_rel.
    apply (supported_rel_subset (dom (x ¬ R1 ++ E))); [reflexivity|].
    eapply RLogic_strong_supported; eauto.
    simpl; split; auto.
  - intros y Hy.
    apply (RLogic_strong_rename y x) in H2; auto.
    + unfold lambda_rel.
      rewrite (subst_intro x).
      × rewrite open_close. assumption.
      × rewrite fv_close. auto.
    + simpl; split; auto.
Qed.

Lemma RLogicMatch_exists E t x1 t1 x2 t2 R R1 R2:
  well_supported_env (x1 ¬ (RelCompose R (RelSumL RelEqVal RelBot)) ++ E) →
  well_supported_env (x2 ¬ (RelCompose R (RelSumL RelBot RelEqVal)) ++ E) →
  RLogic_strong E t R →
  x1 `notin` dom E →
  RLogic_strong (x1 ¬ (RelCompose R (RelSumL RelEqVal RelBot)) ++ E) t1 R1 →
  x2 `notin` dom E →
  RLogic_strong (x2 ¬ (RelCompose R (RelSumL RelBot RelEqVal)) ++ E) t2 R2 →
  RLogic_strong E (Match t (close x1 t1) (close x2 t2))
        (RelUnion
           (RelLet_strong (dom E) (lambda_rel x1 R1) (RelCompose R (RelSumL RelEqVal RelBot)))
           (RelLet_strong (dom E) (lambda_rel x2 R2) (RelCompose R (RelSumL RelBot RelEqVal)))
        ).
Proof.
  intros HsuppE1 HsuppE2 HRLogic_strong Hx1 HRLogic1 Hx2 HRLogic2.
  apply RLogicMatch_strong; auto.
  - apply parametric_family_rel_lambda_rel.
    apply (supported_rel_subset (dom (x1 ¬ (RelCompose R (RelSumL RelEqVal RelBot)) ++ E))); [reflexivity|].
    eapply RLogic_strong_supported; eauto.
  - apply parametric_family_rel_lambda_rel.
    apply (supported_rel_subset (dom (x2 ¬ (RelCompose R (RelSumL RelBot RelEqVal)) ++ E))); [reflexivity|].
    eapply RLogic_strong_supported; eauto.
  - intros y Hy.
    apply (RLogic_strong_rename y x1) in HRLogic1; auto.
    unfold lambda_rel.
    rewrite (subst_intro x1).
    + rewrite open_close. assumption.
    + rewrite fv_close. auto.
  - intros y Hy.
    apply (RLogic_strong_rename y x2) in HRLogic2; auto.
    unfold lambda_rel.
    rewrite (subst_intro x2).
    + rewrite open_close. assumption.
    + rewrite fv_close. auto.
Qed.

Lemma RLogic_weaken E t R:
  well_supported_env E →
  RLogic_strong E t R →
  RLogic E t R.
Proof.
  intros Hsupp H. induction H.
  - eapply RLogicEquiv; eauto.
  - apply RLogicInter; auto.
  - eapply RLogicSub; auto.
  - eapply RLogicSelf; auto.
  - eapply RLogicGather; auto.
  - eapply RLogicVar; eauto.
  - pick fresh x for (dom E `union` fv t2).
    assert (well_supported_env ([(x, R1)] ++ E)) as Hsupp1.
    { simpl; split; auto. eauto with supported_rel. }
    rewrite <- (close_open t2 x); auto.
    rewrite <- (lambda_rel_ext (dom E) x R2); auto.
    rewrite RelLet_rewrite; auto.
    + apply RLogicLet; auto.
    + simpl in Hsupp1. tauto.
  - pick fresh x for (dom E `union` fv t).
    assert (well_supported_env ([(x, R1)] ++ E)) as Hsupp1.
    { simpl; split; auto with supported_rel. }
    rewrite <- (close_open t x); auto.
    rewrite <- (lambda_rel_ext (dom E) x R2); auto.
    rewrite RelLam_rewrite; eauto.
    apply RLogicLam; auto.
  - eapply RLogicApp; eauto.
  - eapply RLogicUnit; eauto.
  - eapply RLogicPair; eauto.
  - eapply RLogicFst; eauto.
  - eapply RLogicSnd; eauto.
  - eapply RLogicInjL; eauto.
  - eapply RLogicInjR; eauto.
  - pick fresh x for (dom E `union` fv t1 `union` fv t2).
    rewrite <- (close_open t1 x); auto.
    rewrite <- (close_open t2 x); auto.
    rewrite <- (lambda_rel_ext (dom E) x R1); auto.
    rewrite <- (lambda_rel_ext (dom E) x R2); auto.
    assert (supported_rel (dom E) R) by eauto with supported_rel.
    repeat rewrite RelLet_rewrite; auto with supported_rel.
    apply RLogicMatch; auto.
    + apply H1; auto. simpl; split; auto with supported_rel.
    + apply H3; auto. simpl; split; auto with supported_rel.
Qed.

Lemma RLogic_strengthen E t R:
  well_supported_env E →
  RLogic E t R →
  RLogic_strong E t R.
Proof.
  intros Hsupp H. induction H.
  - eapply RLogicEquiv_strong; eauto.
  - apply RLogicInter_strong; eauto.
  - eapply RLogicSub_strong; eauto.
  - eapply RLogicSelf_strong; eauto.
  - eapply RLogicGather_strong; eauto.
  - eapply RLogicVar_strong; eauto.
  - assert (well_supported_env ([(x, R1)] ++ E)).
    { simpl; split; auto. eauto with supported_rel. }
    rewrite <- RelLet_rewrite; eauto with supported_rel.
    eapply RLogicLet_exists; eauto.
  - assert (well_supported_env (x ¬ R1 ++ E)).
    { simpl; split; auto with supported_rel. }
    rewrite <- RelLam_rewrite; eauto.
    eapply RLogicLam_exists; eauto.
  - eapply RLogicApp_strong; eauto.
  - eapply RLogicUnit_strong; eauto.
  - eapply RLogicPair_strong; eauto.
  - eapply RLogicFst_strong; eauto.
  - eapply RLogicSnd_strong; eauto.
  - eapply RLogicInjL_strong; eauto.
  - eapply RLogicInjR_strong; eauto.
  - assert (well_supported_env ([(x1, RelCompose R (RelSumL RelEqVal RelBot))] ++ E)).
    { simpl; split; eauto with supported_rel. }
    assert (well_supported_env ([(x2, RelCompose R (RelSumL RelBot RelEqVal))] ++ E)).
    { simpl; split; eauto with supported_rel. }
    repeat rewrite <- RelLet_rewrite; eauto with supported_rel.
    eapply RLogicMatch_exists; eauto with supported_rel.
Qed.

Lemma RLogic_strong_wf E t R:
  wf_env_rel E →
  RLogic_strong E t R →
  wf_rel (dom E) R.
Proof.
  intros Hwf H.
  apply RLogic_weaken in H; auto.
  eapply RLogic_wf; eassumption.
Qed.