- degree assignment, static type assignment, iterated static type

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
index 0c899ad444fca856e47f68de32d0cfcaea081996..acdc78ac6533de4c23c51443a9e7a335b3dde4eb 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
@@ -70,8 +70,8 @@ definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) ….
 | #K0 #l1 #l2 * [ #l01 ] #H1 * [1,3: #l02 ] #H2 //
   [ < H2 in H1; -H2 #H
     lapply (nexts_inj … H) -H #H destruct //
-  | elim (H1 ?) /2 width=2/
-  | elim (H2 ?) /2 width=2/
+  | elim H1 /2 width=2/
+  | elim H2 /2 width=2/
   ]
 | #k0 #l0 *
   [ #l #H destruct elim l -l normalize /2 width=1/