X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Flstas_da.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Flstas_da.ma;h=8b11d1dc0199ea32e7a1ae6dc451c1f00dbd9071;hb=7de928055eb4f717303fa36e287196c6d93cea78;hp=c1726ff5d863558d1d8b762bf6c82c1d7049d877;hpb=db4fa4436863ec774b70787659f749542908f227;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma
index c1726ff5d..8b11d1dc0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_da.ma
@@ -25,3 +25,16 @@ lemma lstas_da_conf: ∀h,g,G,L,T,U,l1. ⦃G, L⦄ ⊢ T •*[h, l1] U →
 #l1 #U #U0 #_ #HU0 #IHTU #l2 #HT
 <minus_plus /3 width=3 by da_sta_conf/
 qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lstas_inv_refl_pos: ∀h,G,L,T,l. ⦃G, L⦄ ⊢ T •*[h, l+1] T → ⊥.
+#h #G #L #T #l #H elim (lstas_inv_step_sn … H)
+#U #HTU #_ elim (sta_da_ge … (l+1) HTU) -U
+#g #l0 #HT #Hl0 lapply (lstas_da_conf … H … HT) -H
+#H0T lapply (da_mono … HT … H0T) -h -G -L -T
+#H elim (discr_x_minus_xy … H) -H
+[ #H destruct /2 width=3 by le_plus_xSy_O_false/
+| -Hl0 <plus_n_Sm #H destruct 
+]
+qed-.