fact: Definition epsilon_def' A {IA:Inhab A} (P:A->Prop) : { x : A | (exists y, P y) -> P x } := match classicT (exists y, P y) with | left H => indefinite_description (let (x,H0) := H in ex_intro (fun x0 => (exists y, P y) -> P x0) x (fun N => H0)) | right H => exist (fun x => (exists y, P y) -> P x) arbitrary (fun N => False_ind (P arbitrary) (H N)) end.
imports: TLC(LibTactics LibLogic LibRelation)