split <;> simp_all[denote, cfold]
case and
a✝ : Ty
l r : Exp Ty.bool
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
      | bConst n, bConst m => bConst (n && m)
      | x, x_1 => and (cfold l) (cfold r))
no goals