[RFC] Implement Boolean-to-Prop coercion using `Bool.asProp`

A while ago, Sebastian suggested[1] that we should redefine the Boolean-to-Prop coercion using a dedicated function. This recently came up again[3] because we're porting material about List.filter, which is now defined on Booleans and thus exercises the coercion heavily.

def Bool.asProp (b : Bool) : Prop :=
  b = true

instance : Coe Bool Prop where
  coe := Bool.asProp

Pros:

1. No accidental simplification of ¬ b = true to b = false (which requires duplication of simp lemmas).
2. decide b = b is defeq (after #2038)
3. Pretty-printing and norm_cast work out-of-the-box.

Cons:

1. simp only [h] no longer works as well for a hypothesis h : b with b : Bool.

Original proposal: [1] https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/rfc.3A.20theorem.20names/near/240161960
Other threads:
[2] https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/BEq.20Subtype/near/296650727
[3] https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Prop.20-.3E.20Bool.20regression/near/321996465

Start by reviewing the proposed Bool.asProp definition and the existing Boolean-to-Prop coercion. The issue names no files, tests, or entry points, so locate the coercion implementation and related tests before deciding how the listed pros and cons affect the design. Done means implementing the coercion with Bool.asProp and validating the behavior described in the proposal.