-#p elim p -p
-[ //
-| * [ #n * [| #l ]] [|*: #p ] #IH #f #q
- [ <lift_d_empty_sn <lift_d_empty_sn >lift_lcons_alt >lift_append_rcons_sn
- <IH <IH -IH <list_append_rcons_sn //
- | <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
- | <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
- <IH <IH -IH <list_append_rcons_sn //
- | <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
- <IH <IH -IH <list_append_rcons_sn //
- | <lift_S_sn <lift_S_sn >lift_lcons_alt >lift_append_rcons_sn
- <IH <IH -IH <list_append_rcons_sn //
- ]
+#p @(path_ind_lift … p) -p // [ #n #l #p |*: #p ] #IH #f #q
+[ <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
+| <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
+ <IH <IH -IH <list_append_rcons_sn //
+| <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
+ <IH <IH -IH <list_append_rcons_sn //
+| <lift_S_sn <lift_S_sn >lift_lcons_alt >lift_append_rcons_sn
+ <IH <IH -IH <list_append_rcons_sn //