Tactic tweaks

[robdockins]

Minor tactic improvements. trivial can now prove more things (reflexive equalities up to conversion), and there is a new experimental goal_exact tactic that allows the user to directly provide a proof term, similar to the core_thm top-level command.

We also tweak the error message from termToProp to give a hint when the user has used lambdas instead of Pis to state a proposition.

[robdockins]

With these changes, the following script will now succeed:

prove_core trivial "(n : Nat) -> (x : Vec n Bool) -> Eq Integer (sbvToInt n x) (toSignedInteger (TCNum n) x)";
prove_core trivial "Eq Nat (addNat 10 32) (mulNat 21 2)";
prove_core trivial "(n : Nat) -> Eq Nat n (addNat 0 n)";

[brianhuffman]

Looks good.