Library CoLoR.Util.Logic.DepChoicePrf

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2007-08-08
proof of dependent choice in classical logic + axiom of choice

Set Implicit Arguments.


Section S.

  Variables (A : Type) (a : A) (R : relation A) (h : left_total R).

  Definition next_elt x := proj1_sig (h x).

  Inductive G : nat -> A -> Prop :=
  | G0 : G 0 a
  | GS : forall i x, G i x -> G (S i) (next_elt x).

  Lemma G_is_classic_left_total : classic_left_total G.

  Lemma G_is_functional : functional G.

  Lemma choice_imply_dep_choice : exists f, IS R f.

End S.