q●↑[f]p = ↑❨(λg,p. proj_path g (q●p)), f, p❩.
#p @(path_ind_lift … p) -p // [ #n #l #p |*: #p ] #IH #f #q
[ <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
q●↑[f]p = ↑❨(λg,p. proj_path g (q●p)), f, p❩.
#p @(path_ind_lift … p) -p // [ #n #l #p |*: #p ] #IH #f #q
[ <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //