add work on fixing equivs, john major equality, proofs at the type-level