Qcert.NNRC.Typing.TcNNRCShadow

Section TcNNRCShadow.




  Context {m:basic_model}.

  Lemma nnrc_type_remove_duplicate_env l v x l' x' l'' e τ:
    nnrc_type (l ++ (v,x)::l' ++ (v,x')::l'') e τ ↔
    nnrc_type (l ++ (v,x)::l' ++ l'') e τ.

 Lemma nnrc_type_remove_free_env l v x l' e τ :
          ¬ In v (nnrc_free_vars e) →
          (nnrc_type (l ++ (v,x)::l') e τ ↔ nnrc_type (l ++ l') e τ).

  Lemma nnrc_type_swap_neq l1 v1 x1 v2 x2 l2 e τ :
    v1 ≠ v2 →
    (nnrc_type (l1++(v1,x1)::(v2,x2)::l2) e τ ↔
     nnrc_type (l1++(v2,x2)::(v1,x1)::l2) e τ).

  Lemma nnrc_type_cons_subst e Γ v τ₀ v' τ :
    ¬ (In v' (nnrc_free_vars e)) →
    ¬ (In v' (nnrc_bound_vars e)) →
    (nnrc_type ((v',τ₀)::Γ) (nnrc_subst e v (NNRCVar v')) τ ↔
     nnrc_type ((v,τ₀)::Γ) e τ).

  Lemma nnrc_type_cons_subst_disjoint e e' Γ v τ₀ τ :
    disjoint (nnrc_bound_vars e) (nnrc_free_vars e') →
         nnrc_type Γ e' τ₀ →
         nnrc_type ((v,τ₀)::Γ) e τ →
         nnrc_type Γ (nnrc_subst e v e') τ.

  Lemma nnrc_type_rename_pick_subst sep renamer avoid e Γ v τ₀ τ :
         (nnrc_type ((nnrc_pick_name sep renamer avoid v e,τ₀)::Γ) (nnrc_rename_lazy e v (nnrc_pick_name sep renamer avoid v e)) τ ↔
         nnrc_type ((v,τ₀)::Γ) e τ).

  Theorem unshadow_type sep renamer avoid Γ n τ :
    nnrc_type Γ n τ ↔ nnrc_type Γ (unshadow sep renamer avoid n) τ.

End TcNNRCShadow.