X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Fstream_eq.ma;h=47f441dd0b1f602a2dad0e37788d40b2c3b522dc;hb=48cd63fc7f4415925582eae224a36a9c1bb3cc06;hp=1e13207763f9d5a6cbf892da04afbb07cf4bd5ea;hpb=55c768d7e45babb300b5010463ba3196a68f1bbe;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma
index 1e1320776..47f441dd0 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma
@@ -55,6 +55,7 @@ lemma stream_eq_repl_sym (A) (R):
 
 (* Basic inversions *********************************************************)
 
+(*** eq_inv_seq_aux *)
 lemma stream_eq_inv_cons_bi (A):
       ∀t1,t2. t1 ≗{A} t2 →
       ∀u1,u2,b1,b2. b1⨮u1 = t1 → b2⨮u2 = t2 →