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