X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fnta%2Fnta.etc;h=8df1f8f5ebc40e31b7db10b2f30e989332e1e20e;hb=de3a41b9a4e51dc1b09adce800273adf5ffa1215;hp=db33815a77fa151349bff20002d1e1d8f0e01768;hpb=0c302a9fda708e5019e48d14c5419a8a65190745;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
index db33815a7..8df1f8f5e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
@@ -9,6 +9,14 @@ lemma nta_pure
 (* Basic_2A1: was: nta_inv_bind1 ntaa_inv_bind1 *)
 lemma nta_inv_bind_sn
 
+(* Basic_1: was by definition: ty3_abst *)
+(* Basic_2A1: was by definition: nta_ldec *)
+lemma nta_ldec_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
@@ -18,3 +26,35 @@ lemma nta_cast_alt: ∀h,L,T,W,U. ⦃h, L⦄ ⊢ T  : W → ⦃h, L⦄ ⊢ T : U
 lapply (nta_mono … HTW … HTU) #HWU
 elim (nta_fwd_correct … HTU) -HTU /3 width=3/
 qed.
+
+lemma nta_ind_alt: ∀h. ∀Q:lenv→relation term.
+   (∀L,k. Q L ⋆k ⋆(next h k)) →
+   (∀L,K,V,W,U,i.
+      ⇩[O, i] L ≡ K.ⓓV → ⦃h, K⦄ ⊢ V : W → ⇧[O, i + 1] W ≡ U →
+      Q K V W → Q L (#i) U
+   ) →
+   (∀L,K,W,V,U,i.
+      ⇩[O, i] L ≡ K.ⓛW → ⦃h, K⦄ ⊢ W : V → ⇧[O, i + 1] W ≡ U →
+      Q K W V → Q L (#i) U
+   ) →
+   (∀I,L,V,W,T,U.
+      ⦃h, L⦄ ⊢ V : W → ⦃h, L.ⓑ{I}V⦄ ⊢ T : U →
+      Q L V W → Q (L.ⓑ{I}V) T U → Q L (ⓑ{I}V.T) (ⓑ{I}V.U)
+   ) →
+   (∀L,V,W,T,U.
+      ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ (ⓛW.T):(ⓛW.U) →
+      Q L V W →Q L (ⓛW.T) (ⓛW.U) →Q L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
+   ) →
+   (∀L,V,W,T,U.
+      ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ (ⓐV.U) : W →
+      Q L T U → Q L (ⓐV.U) W → Q L (ⓐV.T) (ⓐV.U)
+   ) →
+   (∀L,T,U,W.
+      ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W →
+      Q L T U → Q L U W → Q L (ⓝU.T) U
+   ) →
+   (∀L,T,U1,U2,V2.
+      ⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 →
+      Q L T U1 →Q L U2 V2 →Q L T U2
+   ) →
+   ∀L,T,U. ⦃h, L⦄ ⊢ T : U → Q L T U.