bad_unification_hint.lean:7:13: error: invalid unification hint, failed to unify pattern after unifying constraints
bad_unification_hint.lean:12:13: error: invalid unification hint, failed to unify constraint #1
