X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Fstreams.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Fstreams.ma;h=38540eecdeeed3a5aa209426e97a9405a3bf3df5;hb=802e118337ebd0f8b732d4939973aae6415b5bec;hp=4bb3883cebdadf3b4ef3f4b113be6fa506caab06;hpb=a961a1237063702ed9c32a9a4b7994671cb40818;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma
index 4bb3883ce..38540eecd 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams.ma
@@ -31,11 +31,14 @@ coinductive eq_stream (A): relation (stream A) ≝
 interpretation "extensional equivalence (nstream)"
    'ExtEq A t1 t2 = (eq_stream A t1 t2).
 
+definition eq_stream_repl (A) (R:relation …) ≝
+                          ∀t1,t2. t1 ≐⦋A⦌ t2 → R t1 t2.
+
 definition eq_stream_repl_back (A) (R:predicate …) ≝
-                               ∀t1,t2. t1 ≐⦋A⦌ t2 → R t1 → R t2.
+                               ∀t1. R t1 → ∀t2. t1 ≐⦋A⦌ t2 → R t2.
 
 definition eq_stream_repl_fwd (A) (R:predicate …) ≝
-                              ∀t1,t2. t2 ≐⦋A⦌ t1 → R t1 → R t2.
+                              ∀t1. R t1 → ∀t2. t2 ≐⦋A⦌ t1 → R t2.
 
 (* Basic inversion lemmas ***************************************************)