Library hydras.Ackermann.folLogic2

From Coq Require Import Ensembles List Arith.

From hydras.Ackermann Require Import ListExt folProp folProof
  folLogic subProp folReplace.
Import FolNotations.

Section More_Logic_Rules.

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.

Lemma rebindForall (T : System) (a b : nat) (f : Formula):
  ¬ In b (freeVarF (forallH a f)) →
  SysPrf T ((allH a, f) ↔
              (allH b, (substF f a v#b)))%fol.

Lemma rebindExist (T : System) (a b : nat) (f : Formula):
  ¬ In b (freeVarF (existH a f)) →
  SysPrf T (iffH (existH a f) (existH b (substF f a (var b)))).

Lemma subSubTerm (t : Term) (v1 v2 : nat) (s1 s2 : Term):
  v1 ≠ v2 →
  ¬ In v1 (freeVarT s2) →
  substT (substT t v1 s1) v2 s2 =
    substT (substT t v2 s2) v1 (substT s1 v2 s2).

Lemma subSubTerms (n : nat) (ts : Terms n) (v1 v2 : nat) (s1 s2 : Term):
  v1 ≠ v2 →
  ¬ In v1 (freeVarT s2) →
  substTs (substTs ts v1 s1) v2 s2 =
    substTs (substTs ts v2 s2) v1 (substT s1 v2 s2).

Lemma subSubFormula (f : Formula) (v1 v2 : nat) (s1 s2 : Term):
 v1 ≠ v2 →
 ¬ In v1 (freeVarT s2) →
 ∀ T : System,
 SysPrf T
   (iffH (substF (substF f v1 s1) v2 s2)
      (substF (substF f v2 s2) v1
         (substT s1 v2 s2))).

End More_Logic_Rules.