- Inserted additional check for equality types in check_mode_clause that
avoids ill-typed code to be generated.
- Mode inference algorithm now outputs additional diagnostic messages.
Goal "sum n + sum n = n*(Suc n)";
by(induct_tac "n" 1);
by(Auto_tac);