File FreshnessApplicationCtx

From MatchingLogic Require Export Substitution
                                  Freshness
                                  ApplicationContext.

Import Substitution.Notations.

Section lemmas.
  Context {Σ : Signature}.
  Open Scope ml_scope.

  Lemma evar_is_fresh_in_subst_ctx x AC p:
    evar_is_fresh_in x (subst_ctx AC p)
    ↔ (evar_is_fresh_in x p ∧ x ∉ AC_free_evars AC).

  Lemma wf_ex_eq_sctx_eo AC x p:
    well_formed (patt_exists p) = true →
    well_formed (patt_exists ((subst_ctx AC (p^{evar: 0 ↦ x}))^{{evar: x ↦ 0}})) = true.

  Lemma subst_ctx_bevar_subst AC p q n:
  subst_ctx AC (p^[evar: n ↦ q]) = (subst_ctx AC p)^[evar: n ↦ q].

End lemmas.