proposition: Lemma classicT_inhabited : inhabited (forall (P : Type), P + (P -> False)).
proof: 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] | ]; [exists (Witness x) | exists NoWitness]; auto. } constructor. intros P; specialize (H P); destruct (f P); [subst | ]; auto. Qed.
imports: Coq(Logic.Classical_Prop Logic.ClassicalChoice Logic.EqdepFacts Logic.FunctionalExtensionality )