#n #p @(path_ind_lift ā¦ p) -p // [ #m #l #p |*: #p ] #IH #f
[ <lift_rmap_d_sn <lift_path_d_lcons_sn //
| <lift_rmap_L_sn <lift_path_L_sn <IH //
#n #p @(path_ind_lift ā¦ p) -p // [ #m #l #p |*: #p ] #IH #f
[ <lift_rmap_d_sn <lift_path_d_lcons_sn //
| <lift_rmap_L_sn <lift_path_L_sn <IH //