remove e, E from SHA_equiv_pad so the main theorem compiles; remove old induction theorem