(* LIFT FOR PATH ************************************************************)
(* Constructions with tr_uni ************************************************)
(* LIFT FOR PATH ************************************************************)
(* Constructions with tr_uni ************************************************)