deleting EProver2 (going to use EProver3)
renaming EProver3 to EProver2

+ fixed type for Learn_sound.
adding a generic lemma

- need to convert AutoProver3 to use this.