proposition: Lemma D0 : forall i, SysPrf _ (Empty_set _) ( ~ forallH i (P (v#i)) -> exH i, (~ (P (v#i))))%fol.
proof: Proof. intro i; apply cp2, impI, forallI. - intros [f [H H0]]; inversion H0. subst; inversion H1; subst. inversion H1; subst; simpl in H. destruct (Nat.eq_dec i i). + inversion H. + now destruct n. - apply nnE; assert (H:(~ ~ (P (v#i)))%fol = (substF (~ ~ (P (v#i))) i (v#i))%fol). { cbn; destruct (Nat.eq_dec i) as [_ | n]. auto. now destruct n. } rewrite H; apply forallE; rewrite <- H; apply Axm. right; split. Qed.
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)