proposition: Lemma bool_decide_true `{dec : Decision P} : bool_decide P ≡ true ↔ P.
proof: Proof. unfold bool_decide. split; intro; destruct dec; firstorder with bool. Qed.
imports: MathClasses.interfaces.canonical_names MathClasses.misc.util