Improve check error message and document query-based semantics for constructor terms

[Copilot]

check runs a query against existing e-graph state — constructor terms must already be present for a check to succeed, unlike primitives. This mismatch between expectation and behavior produced unhelpful errors with no indication of the root cause.

Changes

• Clearer error message: CheckError now reads "Check failed (are the relevant terms present in the e-graph?)" instead of the bare "Check failed".
• Documentation: Command::Check doc comment now explicitly states that eqsort constructor terms must be pre-existing in the e-graph, with a before/after example contrasting in-graph vs. out-of-graph term behavior.
• New test (check-constructor-not-in-egraph.egg): Covers the failing case from the issue, successful check after let-binding, equality between two variables pointing to the same constructor term, and continued failure for unintroduced terms.

Example

(datatype Math)
(constructor Num (i64) Math)

(fail (check (= (Num 6) (Num 6))))  ;; (Num 6) not in e-graph yet

(let x (Num 6))
(check (= x (Num 6)))               ;; now succeeds

(let y (Num 6))
(check (= x y))                     ;; same term, equality holds

Error before introducing the term:

In 3:1-27 of stdin: (check (= (Num 6) (Num 6)))
Check failed (are the relevant terms present in the e-graph?): 
(= (Num 6) (Num 6))