proposition: Lemma subst_te_open_ee_rec : forall e1 e2 Z P k, subst_te Z P (open_ee_rec k e2 e1) = open_ee_rec k (subst_te Z P e2) (subst_te Z P e1).
proof: Proof. Proof with auto. induction e1; intros e2 Z P k; simpl; f_equal... Case "exp_bvar". destruct (k === n)... Qed.
imports: Fsub.Fsub_LetSum_Definitions