From Coq Require Import
  Logic.Classical_Prop
  Logic.ClassicalChoice
  Logic.EqdepFacts
  Logic.FunctionalExtensionality
.

(* Must be imported to use ddestruction *)
From Coq Require Export
  Program.Equality
.

Set Implicit Arguments.

(* The following tactics may be used:
   - dependent destruction
   - dependent induction *)
Ltac ddestruction :=
  repeat lazymatch goal with | H : existT _ _ _ = _ |- _ ⇒ dependent destruction H end.

(* Consequence of UIP; used by tactic dependent destrcution *)
Definition eq_rect_eq := Eqdep.Eq_rect_eq.eq_rect_eq.

Definition classic := Classical_Prop.classic.

Definition choice := ClassicalChoice.choice.

Definition functional_extensionality := @FunctionalExtensionality.functional_extensionality.

(* From Coq.Logic.ChoiceFacts *)
Definition GuardedFunctionalChoice_on {A B} :=
  ∀ P : A → Prop, ∀ R : A → B → Prop,
    inhabited B →
    (∀ x : A, P x → ∃ y : B, R x y) →
    (∃ f : A→B, ∀ x, P x → R x (f x)).
Axiom guarded_choice : ∀ {A B}, @GuardedFunctionalChoice_on A B.

Inductive mwitness : Type :=
| Witness (P : Type) (_ : P)
| NoWitness.

Lemma classicT_inhabited : inhabited (∀ (P : Type), P + (P → False)).
Proof.
  destruct (choice (fun (P : Type) (b : mwitness) ⇒
    match b with @Witness Q _ ⇒ P = Q | NoWitness ⇒ P → False end)) as [f H].
  { intros P; destruct (classic (inhabited P)) as [[x] | ];
      [∃ (Witness x) | ∃ NoWitness]; auto. }
  constructor. intros P; specialize (H P); destruct (f P); [subst | ]; auto.
Qed.