X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fygt.ma;h=43cc6d0551896bcc8b19a3b6e3a74e0a0ce74603;hb=4eebf1cf684c8a7946b71174ee6145673af49309;hp=0e4ed9f64c5352ef9a3d91ee4597c1dbcce76409;hpb=d7ccf1bd91637d3c59a285df6f215ecfde2a2450;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
index 0e4ed9f64..43cc6d055 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
@@ -83,19 +83,6 @@ lemma cprs_ygt: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥
 ]
 qed.
 
-lemma sstas_ygt: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → (T1 = T2 → ⊥) →
-                 ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄.
-#h #g #G #L #T1 #T2 #H @(sstas_ind … H) -T2
-[ #H elim H //
-| #T #T2 #l #_ #HT2 #IHT1 #HT12 -HT12
-  elim (term_eq_dec T1 T) #H destruct
-  [ -IHT1 /3 width=2/
-  | lapply (IHT1 … H) -IHT1 -H #HT1
-    @(ygt_strap1 … HT1) -HT1 /2 width=2/
-  ]
-]
-qed.
-
 lemma lsubsv_ygt: ∀h,g,G,L1,L2,T. G ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) →
                   ⦃G, L1, T⦄ >[h, g] ⦃G, L2, T⦄.
 /4 width=1/ qed.