+
+lemma unwind2_path_after_lift (p) (f1) (f2):
+ ▼[f2]↑[f1]p = ▼[f2∘f1]p.
+#p @(path_ind_unwind … p) -p // [ #n #l ] #p #IH #f1 #f2
+[ <lift_path_d_sn <unwind2_path_d_lcons
+ <lift_path_lcons_prelift <unwind2_path_d_lcons >lift_path_lcons_prelift
+ >IH -IH
+ >(unwind2_path_eq_repl … (tr_compose_assoc …))
+ >(unwind2_path_eq_repl … (tr_compose_assoc …))
+ <unwind2_path_after <unwind2_path_after in ⊢ (???%);
+ /3 width=1 by unwind2_path_eq_repl, eq_f/
+| <lift_path_m_sn <unwind2_path_m_sn <unwind2_path_m_sn //
+| <lift_path_L_sn <unwind2_path_L_sn <unwind2_path_L_sn
+ >tr_compose_push_bi //
+]
+qed.