cases cfold d with simp[denote]
| bConst b => cases b <;> simp
case if_
a✝ α✝ : Ty
d : Exp Ty.bool
l r : Exp α✝
dih : denote d = denote (cfold d)
lih : denote l = denote (cfold l)
rih : denote r = denote (cfold r)
⊢ (if denote (cfold d) = true then denote (cfold l) else denote (cfold r)) =
    denote
      (match cfold d with
      | bConst true => cfold l
      | bConst false => cfold r
      | x => if_ (cfold d) (cfold l) (cfold r))
no goals