X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Fssta.ma;h=ee7a26e22cbbd06a372cc7facff3d45169db022f;hb=8910c1dc3fcc1da950d0c71f0f1a0150c5557520;hp=7ffa93cb4423f776982884ca5d91e5aacd2bfde1;hpb=18df696e2c97546e5d42e86d18691b8546339160;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
index 7ffa93cb4..ee7a26e22 100644
--- 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 →