Every derivation of a well typed program ends in a value or in error. Every well typed constructor has an evaluation rule, checked by inspection of the rule set. There is no Lean proof, and the property is stated without proving it.

Every construction has rules with mutually exclusive premises, and a Core C++ program has at most one result. The evaluation order fixed left to right removes the choice C++17 leaves to the compiler. There is no Lean proof.