partial commit in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / unwind / unwind_gen_eq.ma

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 34cb91a5a2fc9f5806ffc53ac4af20019c38495f..11ddd2d03ddf324ebfcc81a52f7f2df899e4bd83 100644 (file)
--- 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