proposition: Lemma subst_te_expr : forall Z P e, expr e -> type P -> expr (subst_te Z P e).
proof: Proof. Proof with eauto using subst_tt_type. intros Z P e He Hp. induction He; simpl; auto using subst_tt_type; try solve [ econstructor; try instantiate (1 := L `union` singleton Z); intros; try rewrite subst_te_open_ee_var; try rewrite subst_te_open_te_var; instantiate; eauto using subst_tt_type ]. Qed.
imports: Fsub.Fsub_LetSum_Definitions