File ApplicationCtxSubstitution

From MatchingLogic Require Export ApplicationContext
                                  Substitution.

Import MatchingLogic.Substitution.Notations.

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

  Lemma free_evar_subst_subst_ctx_independent AC ϕ Xfr1 Xfr2:
  Xfr1 ∉ free_evars_ctx AC →
  Xfr2 ∉ free_evars_ctx AC →
  (subst_ctx AC (patt_free_evar Xfr1))^[[evar: Xfr1 ↦ ϕ]] =
  (subst_ctx AC (patt_free_evar Xfr2))^[[evar: Xfr2 ↦ ϕ]].

End with_signature.