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 (* Basic_1: was: ty3_gen_lref *)
  17 (* Basic_2A1: was: nta_inv_lref1 *)
  18 lemma nta_inv_lref_sn_drops
  19
  20 (* Advanced properties ******************************************************)
  21
  22 | ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U
  23
  24 lemma nta_cast_alt: ∀h,L,T,W,U. ⦃h, L⦄ ⊢ T  : W → ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ ⓝW.T : U.
  25 #h #L #T #W #U #HTW #HTU
  26 lapply (nta_mono … HTW … HTU) #HWU
  27 elim (nta_fwd_correct … HTU) -HTU /3 width=3/
  28 qed.
  29
  30 lemma nta_ind_alt: ∀h. ∀Q:lenv→relation term.
  31    (∀L,k. Q L ⋆k ⋆(next h k)) →
  32    (∀L,K,V,W,U,i.
  33       ⇩[O, i] L ≡ K.ⓓV → ⦃h, K⦄ ⊢ V : W → ⇧[O, i + 1] W ≡ U →
  34       Q K V W → Q L (#i) U
  35    ) →
  36    (∀L,K,W,V,U,i.
  37       ⇩[O, i] L ≡ K.ⓛW → ⦃h, K⦄ ⊢ W : V → ⇧[O, i + 1] W ≡ U →
  38       Q K W V → Q L (#i) U
  39    ) →
  40    (∀I,L,V,W,T,U.
  41       ⦃h, L⦄ ⊢ V : W → ⦃h, L.ⓑ{I}V⦄ ⊢ T : U →
  42       Q L V W → Q (L.ⓑ{I}V) T U → Q L (ⓑ{I}V.T) (ⓑ{I}V.U)
  43    ) →
  44    (∀L,V,W,T,U.
  45       ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ (ⓛW.T):(ⓛW.U) →
  46       Q L V W →Q L (ⓛW.T) (ⓛW.U) →Q L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
  47    ) →
  48    (∀L,V,W,T,U.
  49       ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ (ⓐV.U) : W →
  50       Q L T U → Q L (ⓐV.U) W → Q L (ⓐV.T) (ⓐV.U)
  51    ) →
  52    (∀L,T,U,W.
  53       ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W →
  54       Q L T U → Q L U W → Q L (ⓝU.T) U
  55    ) →
  56    (∀L,T,U1,U2,V2.
  57       ⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 →
  58       Q L T U1 →Q L U2 V2 →Q L T U2
  59    ) →
  60    ∀L,T,U. ⦃h, L⦄ ⊢ T : U → Q L T U.