LawfulBEq

Stream: std4

[François G. Dorais]

I just submitted a PR implementing LawfulBEq for option types. <https://github.com/leanprover/std4/pull/164> It's a simple PR with no downstream conflicts in Mathlib, so I hope it can be reviewed soon.

We're waiting on the refactoring of Decidable in core. In the mean time it's unclear what to do with BEq and LawfulBEq. There's a lot more missing instances right now. Does anyone have thoughts about this limbo situation?