Require Import Classical.

Parameter causes : Prop -> Prop -> Prop.
Conjecture wf : well_founded causes.
Hint Resolve wf : core.

Definition contingent (P : Prop) :=
  exists Q, causes Q P.

Definition neccessary (P : Prop) :=
  ~ contingent P.

Corollary GOD : exists G, neccessary G.
  apply NNPP.
  intros H.
  apply well_founded_ind with causes; auto.
  - intros x Hx.
    enough (Hg : exists G, neccessary G).
    contradiction.
    exists x.
    intros [y Hy].
    contradiction (Hx y Hy).
  - exact True.
Qed.