proposition: Lemma open_tt_rec_type : forall T U k, type T -> T = open_tt_rec k U T.
proof: Proof. Proof with auto. intros T U k Htyp. revert k. induction Htyp; intros k; simpl; f_equal... Case "typ_all". unfold open_tt in *. pick fresh X. apply (open_tt_rec_type_aux T2 0 (typ_fvar X))... Qed.
imports: Fsub.Fsub_LetSum_Definitions