All Elm Canonical Ast Expressions can be translated to the intermediate verifier AST.

This does not mean/include that it can be translated into a Structure understandable by the SMT Solver.