matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc

   1 (* Basic_1: was by definition: ty3_bind *)
   2 (* Basic_2A1: was by definition: nta_bind ntaa_bind *)
   3 lemma nta_bind
   4
   5 (* Basic_2A1: was by definition: nta_pure ntaa_pure *)
   6 lemma nta_pure
   7
   8 (* Basic_1: was: ty3_gen_bind *)
   9 (* Basic_2A1: was: nta_inv_bind1 ntaa_inv_bind1 *)
  10 lemma nta_inv_bind_sn
  11
  12 (* Basic_1: was by definition: ty3_abst *)
  13 (* Basic_2A1: was by definition: nta_ldec *)
  14 lemma nta_ldec_drops
  15
  16 (* Advanced properties ******************************************************)
  17
  18 | ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U
  19
  20 lemma nta_cast_alt: ∀h,L,T,W,U. ⦃h, L⦄ ⊢ T  : W → ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ ⓝW.T : U.
  21 #h #L #T #W #U #HTW #HTU
  22 lapply (nta_mono … HTW … HTU) #HWU
  23 elim (nta_fwd_correct … HTU) -HTU /3 width=3/
  24 qed.