proposition: Lemma SOME_def {A : Type'} : (@Some A) = (fun a : A => @_mk_option A ((fun a' : A => @CONSTR A (S (NUMERAL 0)) a' (fun n : nat => @BOTTOM A)) a)).
proof: Proof. apply fun_ext; intro a. apply _dest_option_inj. simpl. match goal with [|- ?x = _] => set (r := x) end. unfold _mk_option. assert (h: exists o, @_mk_option_pred A r o). exists (Some a). reflexivity. generalize (ε_spec h). set (o := ε (_mk_option_pred r)). unfold _mk_option_pred. auto. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance