cases cfold p <;> simp[pairOut, denote]
case snd
a✝ α✝ β✝ : Ty
p : Exp (Ty.prod α✝ β✝)
ih : denote p = denote (cfold p)
⊢ (denote (cfold p)).snd =
    denote
      (match pairOut (cfold p) with
      | some p => p.snd
      | none => snd (cfold p))
no goals