include "delayed_updating/substitution/lift_eq.ma".
include "ground/relocation/tr_compose_pap.ma".
include "ground/relocation/tr_compose_pn.ma".
+include "ground/relocation/tr_compose_tls.ma".
(* LIFT FOR PATH ************************************************************)
lemma lift_path_after (p) (f1) (f2):
↑[f2]↑[f1]p = ↑[f2∘f1]p.
-#p elim p -p [| * ] // #p #IH #f1 #f2
-<lift_path_L_sn <lift_path_L_sn <lift_path_L_sn
->tr_compose_push_bi //
+#p elim p -p [| * ] // [ #n ] #p #IH #f1 #f2
+[ <lift_path_d_sn <lift_path_d_sn <lift_path_d_sn //
+| <lift_path_L_sn <lift_path_L_sn <lift_path_L_sn
+ >tr_compose_push_bi //
+]
qed.