split <;> simp_all[denote, cfold]
case plus
a✝ : Ty
l r : Exp Ty.nat
a_ih✝¹ : denote l = denote (cfold l)
a_ih✝ : denote r = denote (cfold r)
⊢ denote l + denote r =
    denote
      (match cfold l, cfold r with
      | nConst n, nConst m => nConst (n + m)
      | x, x_1 => plus (cfold l) (cfold r))
no goals