Use Bool.asProp for coercions

[gebner]

Fixes #2043.

[gebner]

Without this change, we would not inline anything inside

let x_42 := Foo.casesOn x_3
  fun .. => ... here ...

[gebner]

Required mathlib changes are manageable, as expected: https://github.com/leanprover/std4/compare/pr2060?expand=1 https://github.com/leanprover-community/mathlib4/compare/pr2060?expand=1

[gebner]

!bench

[leanprover-bot]

Here are the benchmark results for commit 8b21496.
There were significant changes against commit 345aa6f:

  Benchmark          Metric         Change
  ====================================================
+ qsort              task-clock      -1.4%   (-17.5 σ)
+ qsort              wall-clock      -1.4%   (-17.6 σ)
+ stdlib             instructions    -2.1% (-2365.0 σ)
- stdlib             maxrss           1.1%    (19.7 σ)
+ stdlib             task-clock      -2.5%   (-38.5 σ)
+ stdlib             wall-clock      -2.9%  (-392.4 σ)
- stdlib size        bytes .olean     1.7%
- workspaceSymbols   maxrss           1.1%    (15.4 σ)
+ workspaceSymbols   task-clock      -2.1%   (-10.0 σ)
+ workspaceSymbols   wall-clock      -2.1%   (-10.1 σ)

[fgdorais]

I really like this but please post something on Zulip when merging since this looks like some significant update changes. A few quick hints might help too. Please remember that mathlib is not the only thing downstream 😄

[kim-em]

This hasn't been touched in over a year, and has a merge conflict. I'm closing now; please re-open if you think appropriate.