proposition: Lemma subst_tt_type : forall Z P T, type T -> type P -> type (subst_tt Z P T).
proof: Proof. Proof with auto. intros Z P T HT HP. induction HT; simpl... Case "type_fvar". destruct (X == Z)... Case "type_all". pick fresh Y and apply type_all... rewrite subst_tt_open_tt_var... Qed.
imports: Fsub.Fsub_LetSum_Definitions