proposition: Lemma reduceSub (T : System) (v : nat) (s : Term) (f g : Formula): ~ In_freeVarSys L v T -> SysPrf T (iffH f g) -> SysPrf T (iffH (substF f v s) (substF g v s)).
proof: Proof. revert T v s f g; assert (H: forall (T : System) (v : nat) (s : Term) (f g : Formula), ~ In_freeVarSys L v T -> SysPrf T (iffH f g) -> SysPrf T (impH (substF f v s) (substF g v s))). { intros T v s f g H H0; rewrite <- (subFormulaImp L). apply forallE; apply forallI. - apply H. - apply (iffE1 L), H0. } intros t v s f g H0 H1; apply iffI. - apply H. + apply H0. + apply H1. - apply H; [assumption| now apply iffSym ]. Qed.
imports: Coq(Ensembles Lists.List Peano_dec) hydras.Ackermann(ListExt folProof folLogic folProp)