trace added in a failing invocation of auto :-(

[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..ee7a26e22cbbd06a372cc7facff3d45169db022f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
@@ -34,6 +34,9 @@ inductive ssta (h:sh) (g:sd h): nat → lenv → relation term ≝
 interpretation "stratified static type assignment (term)"
    'StaticType h g l L T U = (ssta h g l L T U).
 
+definition ssta_step: ∀h. sd h → lenv → relation term ≝ λh,g,L,T,U.
+                      ∃l. ⦃h, L⦄ ⊢ T •[g, l+1] U.
+
 (* Basic inversion lemmas ************************************************)
 
 fact ssta_inv_sort1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀k0. T = ⋆k0 →
@@ -79,6 +82,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.