Module Qcert.cNRAEnv.Typing.TcNRAEnvIgnore

Require Import List.
Require Import String.
Require Import Utils.
Require Import DataSystem.
Require Import NRA.
Require Import NRAEq.
Require Import cNRAEnv.
Require Import cNRAEnvEq.
Require Import cNRAEnvIgnore.
Require Import TcNRAEnv.

Section TcNRAEnvIgnore.

  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 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.
      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.
  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 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 H0; clear H0; subst.
      inversion H; clear H; subst.
      econstructor; eauto.
    - inversion H0; clear H0; subst.
      inversion H; clear H; 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.