fact: Fixpoint denote (e : @expr nat) : nat := match e with | NatO => O | NatS x => S (denote x) | LetIn v f => dlet x := denote v in denote (f x) | Var v => v | NatMul x y => denote x * denote y end.
imports: Reify.Common