X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fetc%2Fsnta%2Flsubsn_ldrop.etc;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fetc%2Fsnta%2Flsubsn_ldrop.etc;h=0000000000000000000000000000000000000000;hb=e8998d29ab83e7b6aa495a079193705b2f6743d3;hp=092883783cfb2d37a5817e3ab0d411d7a7e69875;hpb=bde429ac54e48de74b3d8b1df72dfcb86aa9bae5;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_ldrop.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_ldrop.etc
deleted file mode 100644
index 092883783..000000000
--- a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/lsubsn_ldrop.etc
+++ /dev/null
@@ -1,65 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/dynamic/lsubsn.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE TYPE ASSIGNMENT *******)
-
-(* Properties concerning basic local environment slicing ********************)
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubsn_ldrop_O1_conf: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 →
-                            ∀K1,e. ⇩[0, e] L1 ≡ K1 →
-                            ∃∃K2. h ⊢ K1 :⊑[] K2 & ⇩[0, e] L2 ≡ K2.
-#h #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3/
-| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
-  elim (ldrop_inv_O1 … H) -H * #He #HLK1
-  [ destruct
-    elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
-    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
-  | elim (IHL12 … HLK1) -L1 /3 width=3/
-  ]
-| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K1 #e #H
-  elim (ldrop_inv_O1 … H) -H * #He #HLK1
-  [ destruct
-    elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
-    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
-  | elim (IHL12 … HLK1) -L1 /3 width=3/
-  ]
-]
-qed.
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubsn_ldrop_O1_trans: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 →
-                             ∀K2,e. ⇩[0, e] L2 ≡ K2 →
-                             ∃∃K1. h ⊢ K1 :⊑[] K2 & ⇩[0, e] L1 ≡ K1.
-#h #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3/
-| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H
-  elim (ldrop_inv_O1 … H) -H * #He #HLK2
-  [ destruct
-    elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
-    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
-  | elim (IHL12 … HLK2) -L2 /3 width=3/
-  ]
-| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K2 #e #H
-  elim (ldrop_inv_O1 … H) -H * #He #HLK2
-  [ destruct
-    elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
-    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
-  | elim (IHL12 … HLK2) -L2 /3 width=3/
-  ]
-]
-qed.