Library hydras.Ackermann.Deduction

From Coq Require Import Ensembles List.

From hydras.Ackermann Require Import folProof folProp.
Import FolNotations.

Section Deduction_Theorem.

Variable L : Language.
Let Formula := Formula L.
Let Formulas := Formulas L.
Let System := System L.
Let Term := Term L.
Let Terms := Terms L.
Let Prf := Prf L.
Let SysPrf := SysPrf L.

Let list_incl (X: Ensemble Formula) (l: list Formula) :=
    ∀ x, List.In x l → mem _ X x.

Lemma SysPrf_rephrase X F : SysPrf X F ↔ ∃ s (_ : Prf s F), list_incl X s.

Theorem DeductionTheorem :
  ∀ (T : System) (f g : Formula)
         (prf : SysPrf (Ensembles.Add _ T g) f),
    SysPrf T (g → f)%fol.

End Deduction_Theorem.