proposition: Lemma axiom_13 : forall {A : Type'} (a : option A), (@_mk_option A (@_dest_option A a)) = a.
proof: Proof. intros A o. unfold _mk_option. match goal with [|- ε ?x = _] => set (Q := x); set (q := ε Q) end. assert (i : exists q, Q q). exists o. reflexivity. generalize (ε_spec i). fold q. unfold Q, _mk_option_pred. apply _dest_option_inj. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance