(* Basic_1: was: ty3_gen_lref *)
(* Basic_2A1: was: nta_inv_lref1 *)
lemma nta_inv_lref_sn_drops
(* Basic_1: was: ty3_gen_lref *)
(* Basic_2A1: was: nta_inv_lref1 *)
lemma nta_inv_lref_sn_drops
(* Advanced properties ******************************************************)
| ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U
(* Advanced properties ******************************************************)
| ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U