proposition: Lemma rebindExist (T : System) (a b : nat) (f : Formula): ~ In b (freeVarF (existH a f)) -> SysPrf T (iffH (existH a f) (existH b (substF f a (var b)))).
proof: Proof. intro H; unfold existH. apply (reduceNot L); eapply (iffTrans L). - apply (rebindForall T a b (notH f)), H. - rewrite (subFormulaNot L); apply (iffRefl L). Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(ListExt folProp folProof folLogic subProp folReplace)