proposition: Lemma subst_te_open_te_rec : forall e T X U k, type U -> subst_te X U (open_te_rec k T e) = open_te_rec k (subst_tt X U T) (subst_te X U e).
proof: Proof. intros e T X U k WU. revert k. induction e; intros k; simpl; f_equal; auto using subst_tt_open_tt_rec. Qed.
imports: Fsub.Fsub_LetSum_Definitions