-(* Properties with tr_compose ***********************************************)
-
-lemma unwind2_path_after (p) (f1) (f2):
- ▼[f2]▼[f1]p = ▼[f2∘f1]p.
-#p @(path_ind_unwind … p) -p // [ #n #l #p | #p ] #IH #f1 #f2
-[ <unwind2_path_d_lcons <unwind2_path_d_lcons
- >(unwind2_path_eq_repl … (tr_compose_assoc …)) //
-| <(unwind2_path_L_sn … f1) <unwind2_path_L_sn <unwind2_path_L_sn
- >tr_compose_push_bi //
-]
-qed.