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