proposition: Lemma expr_case_from_body : forall e1 e2 e3, expr e1 -> body_e e2 -> body_e e3 -> expr (exp_case e1 e2 e3).
proof: Proof. intros e1 e2 e3 H [J1 J2] [K1 K2]. pick fresh y and apply expr_case; auto. Qed.
imports: Fsub.Fsub_LetSum_Definitions