proposition: Lemma reduceForall (f1 f2 : Formula) (v : nat) (T : System): ~ In_freeVarSys _ v T -> SysPrf T (iffH f1 f2) -> SysPrf T (iffH (forallH v f1) (forallH v f2)).
proof: Proof. intros H H0; apply (iffI L). - apply impForall; [assumption | ]; apply (iffE1 L), H0. - apply impForall; [assumption | ]; apply (iffE2 L), H0. Qed.
imports: Coq(Ensembles Lists.List Peano_dec) hydras.Ackermann(ListExt folProof folLogic folProp)