Special Handling for Eq Conditions

[marcusrossel]

If a rewrite as a condition of the form a = b, then it would be nice if we could check if it is satisfied, without explicitly requiring a fact of this form. For example, this is useful for automated satisfaction of rfl-conditions like 0 = 0, which can pop up in if-then-else expressions.

[marcusrossel]

A relevant example is List.get?_modifyNth_eq in batteries.