proposition: Lemma subst_ee_open_te_rec : forall e P z u k, expr u -> subst_ee z u (open_te_rec k P e) = open_te_rec k P (subst_ee z u e).
proof: Proof. Proof with auto. induction e; intros P z u k H; simpl; f_equal... Case "exp_fvar". destruct (a == z)... apply open_te_rec_expr... Qed.
imports: Fsub.Fsub_LetSum_Definitions