#g #f #p elim p -p // #l #p #IH
<lift_path_rcons <lift_rmap_rcons <unwind2_rmap_rcons <unwind2_rmap_rcons
@(stream_eq_trans … (preunwind2_lift_rmap_after …))
#g #f #p elim p -p // #l #p #IH
<lift_path_rcons <lift_rmap_rcons <unwind2_rmap_rcons <unwind2_rmap_rcons
@(stream_eq_trans … (preunwind2_lift_rmap_after …))