mathlib

e734856a - Add a less synthetic test case for auto-generalisation