(* Note: this is known as the substitution lemma *)
(* Basic_1: was only: ty3_gen_cabbr *)
lemma nta_thin_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 →
(* Note: this is known as the substitution lemma *)
(* Basic_1: was only: ty3_gen_cabbr *)
lemma nta_thin_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 →