Separated parsed, valid patterns from TermLike #2640
Description
The data type TermLike is used to represent all patterns after parsing and validation, and for terms during execution. Because of it is used for all patterns after validation, the type admits many terms which should never appear during execution, such as:
\rewrites\next\implies\floor\ceil\equals\in
We should create a separate type for valid patterns, and restrict the type of terms allowed during execution. This would simplify simplification significantly.