simp_all[denote]
case pair
a✝ α✝ β✝ : Ty
l : Exp α✝
r : Exp β✝
a_ih✝¹ : denote l = denote (cfold l)
a_ih✝ : denote r = denote (cfold r)
⊢ denote l = denote (cfold l) ∧ denote r = denote (cfold r)
no goals