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