X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind_gen_eq.ma;h=11ddd2d03ddf324ebfcc81a52f7f2df899e4bd83;hb=ccbaf3fd118c7c6425b3572a057ccc2941b7762e;hp=34cb91a5a2fc9f5806ffc53ac4af20019c38495f;hpb=9b4e20442ec5a4028cfe2b6fe836c94acdb033b8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma
index 34cb91a5a..11ddd2d03 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma
@@ -19,15 +19,11 @@ include "ground/relocation/tr_pap_eq.ma".
 
 (* Constructions with stream_eq *********************************************)
 
-lemma unwind_gen_eq_repl (p) (f1) (f2):
-      (∀n. f1 n ≗ f2 n) → ◆[f1]p = ◆[f2]p.
-#p @(path_ind_unwind … p) -p // [ #n | #n #l #p |*: #p ] #IH #f1 #f2 #Hf
+lemma unwind_gen_eq_repl (p):
+      stream_eq_repl … (λf1,f2. ◆[f1]p = ◆[f2]p).
+#p @(path_ind_unwind … p) -p // [ #n |*: #p ] #IH #f1 #f2 #Hf
 [ <unwind_gen_d_empty <unwind_gen_d_empty
-  <(tr_pap_eq_repl … (Hf n)) -f2 -IH //
-| <unwind_gen_d_lcons <unwind_gen_d_lcons
-  <(IH … Hf) -f2 -IH //
-| <unwind_gen_m_sn <unwind_gen_m_sn
-  <(IH … Hf) -f2 -IH //
+  <(tr_pap_eq_repl … Hf) -f2 -IH //
 | <unwind_gen_L_sn <unwind_gen_L_sn
   <(IH … Hf) -f2 -IH //
 | <unwind_gen_A_sn <unwind_gen_A_sn