Use nested proof in inductive proof
Simplifiy validEquationProof

With proper variable handling, prop and goal have to be equal
(and not some shady variant of matching).
Inline validEquationProof