-lemma lift_eq_repl_sn (A) (p) (k1) (k2) (f):
- k1 ≗{A} k2 → ↑❨k1, f, p❩ = ↑❨k2, f, p❩.
-#A #p @(path_ind_lift … p) -p [| #n | #n #l0 #q ]
-[ #k1 #k2 #f #Hk <lift_empty <lift_empty //
-|*: #IH #k1 #k2 #f #Hk /2 width=1 by/
+lemma lift_eq_repl (A) (p) (k1) (k2):
+ k1 ≗{A} k2 → stream_eq_repl … (λf1,f2. ↑❨k1, f1, p❩ = ↑❨k2, f2, p❩).
+#A #p @(path_ind_lift … p) -p [| #n #IH | #n #l0 #q #IH |*: #q #IH ]
+#k1 #k2 #f1 #f2 #Hk #Hf
+[ <lift_empty <lift_empty /2 width=1 by/
+| <lift_d_empty_sn <lift_d_empty_sn <(tr_pap_eq_repl … Hf)
+ /3 width=1 by tr_compose_eq_repl, stream_eq_refl/
+| <lift_d_lcons_sn <lift_d_lcons_sn
+ /3 width=1 by tr_compose_eq_repl, stream_eq_refl/
+| /2 width=1 by/
+| /3 width=1 by tr_push_eq_repl/
+| /3 width=1 by/
+| /3 width=1 by/