Close goals of the form n ≠ m when n and m have type nat, char, string, int or fin sz,
and they are literals. It also closes goals of the form n < m, n > m, n ≤ m and n ≥ m for nat.
If the foal is of the form n = m, then it tries to close it using reflexivity.