proposition: Lemma cfoldcorrect: forall t (e: exp t), expDenote e = expDenote (cfold e).
proof: Proof. intros; funelim (cfold e); simpl; intros; try reflexivity; repeat match goal with [ H : expDenote ?e = _ |- context[expDenote ?e]] => rewrite H end; try (match goal with [ |- _ = expDenote ?f] => funelim f end); simpl; repeat match goal with [ H : _ = cfold ?e |- _] => rewrite <- H; simpl end; try reflexivity; repeat match goal with [ |- context[if ?e then _ else _]] => destruct e end; try reflexivity. Qed.
imports: Arith Equations(Equations) Coq.Bool.Bool