/2 width=2 by path_closed_structure_depth/
| lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H0t1
<unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn
/2 width=2 by path_closed_structure_depth/
| lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H0t1
<unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn