update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / steps / rtc_ist_plus.ma

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 c17eec5b6795f050ec319ed3e0424184cd10ea0b..a66a81d29ac882bfb0c8cff1dbb1f3ccee47a1ac 100644 (file)
--- 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-.