File Sorts_ProofSystem

From MatchingLogic Require Export Sorts_Syntax
                                  MLPM
                                  FOEquality_ProofSystem.
Import MatchingLogic.Logic.Notations
       MatchingLogic.Theories.Definedness_Syntax.Notations
       MatchingLogic.Theories.Sorts_Syntax.Notations.


Open Scope list_scope.

Local Lemma simplTest
  {Σ : Signature}
  {syntax : Sorts_Syntax.Syntax}
  (Γ : Theory)
  (φ ψ τ: Pattern)
  (s : symbols) x:
  well_formed (ex , φ) →
  well_formed ψ →
  well_formed τ →
  Definedness_Syntax.theory ⊆ Γ →
  Γ ⊢ ((all ψ , φ) ---> ex ψ , φ)^[[evar:x↦τ]].

Lemma ex_sort_impl_ex
  {Σ : Signature}
  {syntax : Sorts_Syntax.Syntax}
  (Γ : Theory)
  (ϕ : Pattern)
  (s : symbols)
  :
  well_formed (ex , ϕ) →
  Definedness_Syntax.theory ⊆ Γ →
  Γ ⊢ (ex (patt_sym s) , ϕ) ---> (ex , ϕ).

Theorem top_includes_everything {Σ : Signature} {syntax : Sorts_Syntax.Syntax}:
  ∀ (Γ : Theory) (x : evar),
  Definedness_Syntax.theory ⊆ Γ →
  Γ ⊢i patt_free_evar x ∈ml patt_top using AnyReasoning.