proposition: Lemma decide_bool_decide P {Hdec: Decision P} {X : Type} (x1 x2 : X): (if decide P then x1 else x2) = (if bool_decide P then x1 else x2).
proof: Proof. unfold bool_decide, decide. destruct Hdec; reflexivity. Qed.
imports: stdpp(options)