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