Relating the two semantics

• Proof of the implication in the opposite direction requires the formulation of a domain predicate, comDom, for the denotation function.
• An extra complication arises because of nested recursion and the absence of Dybjer's simultaneous inductive-recursive definitions in Coq.
• The equivalence of the operational and the denotational semantics is now stated as follows: