Module Qcert.cNRAEnv.Typing.TcNRAEnvIgnore


Section TcNRAEnvIgnore.
  Require Import List.
  Require Import String.
  Require Import Utils.
  Require Import CommonSystem.
  Require Import NRA.
  Require Import NRAEq.
  Require Import cNRAEnv.
  Require Import 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 τcin τout τenv₁ τenv₂:rtype),
    e ▷ τin >=> τout ⊣ τcenv₁ -> e ▷ τin >=> τout ⊣ τcenv₂.
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 τcin₁ τin₂ τout τenv:rtype),
    e ▷ τin₁ >=> τout ⊣ τcenv -> e ▷ τin₂ >=> τout ⊣ τcenv.
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.