Module TcNRAEnvIgnore

Section TcNRAEnvIgnore.

  Require Import List String.

  Require Import Utils BasicSystem.

  Require Import NRA NRAEq cNRAEnv cNRAEnvEq.

  Require Import cNRAEnvIgnore.
  Require Import TcNRAEnv.

  Local Open Scope nraenv_core_scope.

  Lemma tnraenv_core_ignores_env_swap {m:basic_model} (e:nraenv_core) :
    nraenv_core_ignores_env e ->
    forall τc (τin τout τenv₁ τenv₂:rtype),
    e ▷ τin >=> τout ⊣ τc;τenv₁ -> e ▷ τin >=> τout ⊣ τc;τenv₂.

Proof.

    induction e ; try reflexivity; simpl in *; try congruence; try contradiction; intros.
    - inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0.
      econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0.
      econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0.
      econstructor; eauto.
    - inversion H0; clear H0.
      econstructor; eauto.
    - inversion H0; clear H0.
      econstructor; eauto.
  Qed.

  Lemma tnraenv_core_ignores_id_swap {m:basic_model} (e:nraenv_core) :
    nraenv_core_ignores_id e ->
    forall τc (τin₁ τin₂ τout τenv:rtype),
    e ▷ τin₁ >=> τout ⊣ τc;τenv -> e ▷ τin₂ >=> τout ⊣ τc;τenv.

Proof.

    induction e ; try reflexivity; simpl in *; try congruence; try contradiction; intros.
    - inversion H0; clear H0; intros.
      econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H0; clear H0; subst.
      inversion H; clear H; subst.
      econstructor; eauto.
    - inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H0; clear H0. econstructor; eauto.
    - inversion H0; clear H0. econstructor; eauto.
    - inversion H; clear H.
      inversion H0; clear H0; subst.
      econstructor; eauto.
    - inversion H0; clear H0; subst.
      econstructor; eauto.
  Qed.

End TcNRAEnvIgnore.