- >list_append_rcons_sn in H1n; <reverse_append #H1n
- <(lift_path_head ā¦ H1n) -H1n //
-| lapply (in_comp_lift_path_term f ā¦ Ht1) -Ht2 -Ht1 -H1n
+ <(lift_path_head_closed ā¦ H1k) in ā¢ (??%?); -H1k //
+| lapply (in_comp_lift_path_term f ā¦ Ht1) -Ht2 -Ht1 -H1k