X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Fstreams_hdtl.ma;h=bdc740c82ff42646cbd6fb362c6ac714fa731cf3;hb=91ab6965be539b7ed0f3208e1c1fffd17aa151f7;hp=e23b7bb2d4d246e5e59a2338337503aaf70b5ac5;hpb=5791ee6b64136ecb0a727e32997b33f4bfab2c31;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
index e23b7bb2d..bdc740c82 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_hdtl.ma
@@ -35,6 +35,5 @@ qed.
 
 lemma tln_eq_repl (A) (i): eq_stream_repl A (λt1,t2. tln … i t1 ≐ tln … i t2).
 #A #i elim i -i //
-#i #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq ????? H) -H
-/2 width=1 by/
+#i #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq … H) /2 width=7 by/
 qed.