proposition: Theorem drinkers_thm : SysPrf L (Empty_set _) f.
proof: Proof. Proof with auto with sets. pose (F := forallH 1 (P (v#1))%fol). unfold f; eapply orE with (notH F) F; [apply noMiddle | | ]. - apply impI; assert (SysPrf L (Add (Empty_set _) (~ F)%fol) (exH 1, (~ (P (v#1))))%fol). { replace (exH 1, (~ (P (v#1))))%fol with (~ (forallH 1 (~ (~ (P (v#1))))))%fol. - unfold F; eapply impE. + eapply D01. + apply Axm; right; split. - auto. } + eapply existE with (v:=1). * unfold F; intro H0; destruct H0. destruct H0 as [H0 H1]; inversion H1. -- inversion H2. -- subst. inversion H2. subst; now simpl in H0. * cbn; auto. * eapply H. * apply impI; eapply existI with (v#1)%fol. cbn; apply impI. eapply contradiction with (P (v#1))%fol. -- apply Axm; red ... -- apply Axm; red ... - apply impI; apply existI with (v#0)%fol. cbn; apply impI. apply Axm; red; auto with sets. Qed.
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)