proposition: Remark subFormulaNTEHelp (f g : Formula) (v : nat) (s : Term): SysPrf (Ensembles.Add _ (Empty_set Formula) f) g -> SysPrf (Ensembles.Add _ (Empty_set Formula) (substF f v s)) (substF g v s).
proof: Proof. intro H; apply (impE L) with (substF f v s). - apply (sysWeaken L). rewrite <- (subFormulaImp L). apply forallE. apply forallI. + apply (notInFreeVarSys L). + apply (impI L). apply H. - apply Axm; right; constructor. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)