Definition isaprop_goal X (ig:isaprop X) (f:isaprop X -> X) : X. Proof. intros. exact (f ig). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom.