File ProductSort_ProofSystem

From MatchingLogic Require Export Sorts_ProofSystem
                                  ProductSort.
Import MatchingLogic.Logic.Notations
       MatchingLogic.Theories.Definedness_Syntax.Notations
       MatchingLogic.Theories.Sorts_Syntax.Notations
       MatchingLogic.Theories.ProductSort.Notations.


Open Scope list_scope.

Section productsort.
  Context
      {Σ : Signature}
      (s1 s2 : Pattern)
      (wfs1 : well_formed s1 = true)
      (wfs2 : well_formed s2 = true)
      {syntax : ProductSort.Syntax s1 s2}
    .

  Lemma use_productsort_axiom ax Γ :
      ProductSort.theory s1 s2 wfs1 wfs2 ⊆ Γ →
        Γ ⊢ axiom _ _ ax.

  Theorem prod_sort : ∀ Γ , theory s1 s2 wfs1 wfs2 ⊆ Γ →
                              Γ ⊢ all mlProd(s1,s2), ex s1, ex s2, ( b1 ∷ s1 , b0 ∷ s2 ) =ml b2 .

End productsort.