update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / stream_eq.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_eq.ma
index 1e13207763f9d5a6cbf892da04afbb07cf4bd5ea..47f441dd0b1f602a2dad0e37788d40b2c3b522dc 100644 (file)
--- 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 →