proposition: Lemma cfoldCond_correct : forall t (default : exp' t) n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t), exp'Denote (cfoldCond default tests bodies) = exp'Denote (Cond n tests bodies default).
proof: Proof. unshelve refine_ho (cfoldCond_elim _ _ _ _ _ _ _ _ _ _ _ _ _ _); simpl; intros. all:simpl; simp exp'Denote cond; rewrite ?H, ?Heq, ?Heq0; try rewrite ?Heq in Hind; simp exp'Denote cond; now repeat (match goal with | [ |- context[cond_clause_2 _ _ ?E _] ] => destruct E; simp cond end). Qed.
imports: Arith List Program Equations.Prop.Equations