+(* Basic constructions with structure **************************************)
+
+lemma structure_lift (p) (f):
+ ⊗p = ⊗↑[f]p.
+#p @(path_ind_lift … p) -p // #p #IH #f
+<lift_path_L_sn //
+qed.
+
+lemma lift_structure (p) (f):
+ ⊗p = ↑[f]⊗p.
+#p @(path_ind_lift … p) -p //
+qed.
+
+(* Properties with proper condition for path ********************************)
+
+lemma lift_append_proper_dx (p2) (p1) (f): Ꝕp2 →
+ (⊗p1)●(↑[↑[p1]f]p2) = ↑[f](p1●p2).
+#p2 #p1 @(path_ind_lift … p1) -p1 //
+[ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
+[ elim (ppc_inv_lcons … Hp2) -Hp2 #l #q #H destruct //
+| <lift_path_d_lcons_sn <IH //
+| <lift_path_L_sn <IH //
+| <lift_path_A_sn <IH //
+| <lift_path_S_sn <IH //
+]
+qed-.
+
+(* Advanced constructions with structure ************************************)