mathlib

39ca9a63 - Trying to fix unused arguments by introducing variables. Order of lemmas changed. Also trying to fix simp normal form.