proposition: Lemma subFormulaExch : forall (f : Formula) (T : System) (v1 v2 : nat) (s1 s2 : Term), v1 <> v2 -> ~ In v2 (freeVarT s1) -> ~ In v1 (freeVarT s2) -> SysPrf T (iffH (substF (substF f v1 s1) v2 s2) (substF (substF f v2 s2) v1 s1)).
proof: Proof. intros f T; eapply proj2, proj2. apply subFormulaNTE. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)