mathlib

246f8d57 - Clean up proofs + define length of statement