proposition: Lemma rebindForall (T : System) (a b : nat) (f : Formula): ~ In b (freeVarF (forallH a f)) -> SysPrf T ((allH a, f) <-> (allH b, (substF f a v#b)))%fol.
proof: Proof. intros H; eapply (sysExtend L) with (Empty_set Formula). - intros x H0; destruct H0. - apply (iffI L). + apply (impI L), (forallI L). intros [x [H0 H1]]. destruct H1 as [x H1| x H1]; [ induction H1 | induction H1 ]. * auto. * apply forallE; apply Axm; right; constructor. + apply (impI L), (forallI L). intros [x [H0 H1]] ; destruct H1 as [x H1| x H1]; [induction H1 | induction H1]. * assert (H1: In a (freeVarF (substF f a (var b)))) by (eapply in_remove; apply H0). induction (freeVarSubFormula3 _ _ _ _ _ H1). elim (in_remove_neq _ _ _ _ _ H2). -- auto. -- elim (in_remove_neq _ _ _ _ _ H0). destruct H2 as [H2| H2]. auto. elim H2. * set (A1 := forallH b (substF f a (var b))) in *. rewrite <- (subFormulaId L f a). apply (impE L) with (substF (substF f a (var b)) b (var a)). -- apply (iffE1 L). apply (subFormulaTrans L); apply H. -- apply forallE, Axm; right; constructor. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(ListExt folProp folProof folLogic subProp folReplace)