proposition: Lemma subFormulaTrans : forall (f : Formula) (T : System) (v1 v2 : nat) (s : Term), ~ In v2 (List.remove eq_nat_dec v1 (freeVarF f)) -> SysPrf T (iffH (substF (substF f v1 (var v2)) v2 s) (substF f v1 s)).
proof: Proof. intros f T; eapply proj1, proj2; apply subFormulaNTE. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)