-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