File TEST_proofmode_example

From MatchingLogic.Theories Require Import Definedness_Semantics
                                           Sorts_Syntax
                                           Definedness_ProofSystem.
From MatchingLogic.Utils Require Import stdpp_ext.

Import MatchingLogic.Logic.Notations.
Import MatchingLogic.Theories.Definedness_Syntax.Notations.
Import MatchingLogic.Semantics.Notations.
Import MatchingLogic.DerivedOperators_Syntax.Notations.

Close Scope equations_scope. (* Because of ! *)

Lemma membership_var {Σ : Signature} {syntax : Syntax} :
  ∀ x y Γ,
  theory ⊆ Γ →
  Γ ⊢ patt_free_evar y ∈ml patt_free_evar x ---> patt_free_evar y =ml patt_free_evar x.