Lean tactic: evaluate a closed List term with evalExpr, then kernel-check

To make a reflective SAT tactic generic over any closed P : List (List Clause) (Lean v4.35), evaluate the goal's argument in MetaM with unsafe def evalP (e) := evalExpr (List (List Clause)) tyExpr e, exposed via @[implemented_by evalP] opaque evalPieces. Then write DIMACS, run the solver, and emit Eq.refl true theorems that recompute the pieces in the kernel. Matching the goal: Unsat (List.flatten P) is @List.flatten α P, so use e.app2? List.flatten and take the second component. Do not whnfR the goal type first, or flatten unfolds away. It worked first try on a pigeonhole cardinality system. A satisfiable instance makes CaDiCaL exit 10, so check the exit code and fail loudly.