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 7ffa93cb4423f776982884ca5d91e5aacd2bfde1..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 →