"Lawful" instances

[iamrecursion]

Currently having an instance of a trait (e.g. std::cmp::Eq) tells us nothing about what we can assume about that trait. As things evolve, we may want to look into a set of "Lawful" classes in Lean that allow us to make stronger statements when having an instance of a given trait.

Given the class LawfulX, the user would need to create an instance of the class and show that their impl of the trait X satisfies the "laws".