proposition: Lemma subst_te_intro_rec : forall X e U k, X `notin` fv_te e -> open_te_rec k U e = subst_te X U (open_te_rec k (typ_fvar X) e).
proof: Proof. induction e; intros U k Fr; simpl in *; f_equal; auto using subst_tt_intro_rec. Qed.
imports: Fsub.Fsub_LetSum_Definitions