proposition: Lemma nForall (T : System) (f : Formula) (v : nat) : SysPrf T (exH v, ~ f)%fol -> SysPrf T (~ (allH v, f))%fol.
proof: Proof. intros H; apply impE with (exH v, ~ f)%fol. - apply sysExtend with (Empty_set Formula). intros g H0. destruct H0. apply impI; apply existSys. intros [x [H0 H1]]; destruct H1. simpl in |- *; intro H0. absurd (v = v). + eapply in_remove_neq. apply H0. + reflexivity. + apply impE with (~ f)%fol. * apply cp2, sysWeaken, impI. eapply forallSimp. apply Axm; right; constructor. * apply Axm; right; constructor. - assumption. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)