proposition: Lemma NONE_def {A : Type'} : (@None A) = (@_mk_option A (@CONSTR A (NUMERAL 0) (@ε A (fun v : A => True)) (fun n : nat => @BOTTOM A))).
proof: Proof. 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 None. 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