Definition choice_compute_yes {W : UU} (P : DecidableProposition) (p : P) (yes no : W) : choice P yes no = yes. Proof. intros. unfold choice. choose P a b. - simpl. reflexivity. - simpl. contradicts p b. Defined.
Require Import UniMath.MoreFoundations.Tactics.