File Subseteq_ProofSystem

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


Open Scope list_scope.

Lemma patt_subseteq_trans
    {Σ : Signature}
    {syntax : Definedness_Syntax.Syntax}
    (Γ : Theory)
    (ϕ₁ ϕ₂ ϕ₃ : Pattern)
    :
    well_formed ϕ₁ →
    well_formed ϕ₂ →
    well_formed ϕ₃ →
    Definedness_Syntax.theory ⊆ Γ →
    Γ ⊢ patt_subseteq ϕ₁ ϕ₂ --->
        patt_subseteq ϕ₂ ϕ₃ --->
        patt_subseteq ϕ₁ ϕ₃
.