mathlib

171006b7 - unify_equations: remove trivial hyps generated by injection_with