X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fsteps%2Frtc_ist_plus.ma;h=a66a81d29ac882bfb0c8cff1dbb1f3ccee47a1ac;hp=c17eec5b6795f050ec319ed3e0424184cd10ea0b;hb=f38fd769279794d0ca73c8945eac30e8b42e59be;hpb=0af3592e3a85a4bb82c5c6df259cf9ab117ba0b1

diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_plus.ma
index c17eec5b6..a66a81d29 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_plus.ma
@@ -58,3 +58,9 @@ lemma ist_inv_plus_SO_dx:
 elim (ist_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
 /2 width=3 by ex2_intro/
 qed-.
+
+lemma ist_inv_plus_10_dx: ∀n,c. 𝐓⦃n,c+𝟙𝟘⦄ → ⊥.
+#n #c #H
+elim (ist_inv_plus … H) -H #n1 #n2 #_ #H #_
+/2 width=2 by ist_inv_10/
+qed-.