proposition: Lemma axiom_14' : forall {A : Type'} (r : recspace A), (option_pred r) = ((@_dest_option A (@_mk_option A r)) = r).
proof: Proof. intros A r. apply prop_ext. intro h. apply (@ε_spec _ (_mk_option_pred r)). rewrite option_eq in h. induction h. exists None. reflexivity. exists (Some a''). reflexivity. intro e. rewrite <- e. intros P h. apply h. destruct (_mk_option r); simpl. right. exists t0. reflexivity. left. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance