more service lemmas in nat and lambdadelta

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / ssta.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
index 3cd0134bb35f48f070825e421bc7ec21e34a1ced..7ffa93cb4423f776982884ca5d91e5aacd2bfde1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
@@ -79,6 +79,19 @@ lemma ssta_inv_lref1: ∀h,g,L,U,i,l. ⦃h, L⦄ ⊢ #i •[g, l] U →
                       ).
 /2 width=3/ qed-.
 
+fact ssta_inv_gref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀p0. T = §p0 → ⊥.
+#h #g #L #T #U #l * -L -T -U -l
+[ #L #k #l #_ #p0 #H destruct
+| #L #K #V #W #U #i #l #_ #_ #_ #p0 #H destruct
+| #L #K #W #V #U #i #l #_ #_ #_ #p0 #H destruct
+| #a #I #L #V #T #U #l #_ #p0 #H destruct
+| #L #V #T #U #l #_ #p0 #H destruct
+| #L #W #T #U #l #_ #p0 #H destruct
+qed.
+
+lemma ssta_inv_gref1: ∀h,g,L,U,p,l. ⦃h, L⦄ ⊢ §p •[g, l] U → ⊥.
+/2 width=9/ qed-.
+
 fact ssta_inv_bind1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U →
                          ∀a,I,X,Y. T = ⓑ{a,I}Y.X →
                          ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[g, l] Z & U = ⓑ{a,I}Y.Z.