proposition: Lemma subst_tt_intro_rec : forall X T2 U k, X `notin` fv_tt T2 -> open_tt_rec k U T2 = subst_tt X U (open_tt_rec k (typ_fvar X) T2).
proof: Proof. Proof with congruence || auto. induction T2; intros U k Fr; simpl in *; f_equal... Case "typ_bvar". destruct (k === n)... simpl. destruct (X == X)... Case "typ_fvar". destruct (a == X)... contradict Fr; fsetdec. Qed.
imports: Fsub.Fsub_LetSum_Definitions