/2 width=2 by path_closed_structure_depth/
| lapply (in_comp_unwind2_path_term f … Ht1) -H0t1 -Hb -Hm -Ht2 -Ht1
<unwind2_path_d_dx <tr_pap_succ_nap >list_append_rcons_dx >list_append_assoc
/2 width=2 by path_closed_structure_depth/
| lapply (in_comp_unwind2_path_term f … Ht1) -H0t1 -Hb -Hm -Ht2 -Ht1
<unwind2_path_d_dx <tr_pap_succ_nap >list_append_rcons_dx >list_append_assoc