fact: Fixpoint open_tt_rec (K : nat) (U : typ) (T : typ) {struct T} : typ := match T with | typ_top => typ_top | typ_bvar J => if K == J then U else (typ_bvar J) | typ_fvar X => typ_fvar X | typ_arrow T1 T2 => typ_arrow (open_tt_rec K U T1) (open_tt_rec K U T2) | typ_all T1 T2 => typ_all (open_tt_rec K U T1) (open_tt_rec (S K) U T2) | typ_sum T1 T2 => typ_sum (open_tt_rec K U T1) (open_tt_rec K U T2) end.
imports: Metalib.Metatheory String