- #n #_ cases l [ #m ]
- [ <unwind2_rmap_d_sn <path_head_d_sn <height_d_sn
- <nplus_assoc >IH -IH <tr_compose_xap <tr_uni_xap_succ //
- | <unwind2_rmap_m_sn <path_head_m_sn <height_m_sn //
- | <unwind2_rmap_L_sn <path_head_L_sn <height_L_sn
- <tr_xap_push <npred_succ //
- | <unwind2_rmap_A_sn <path_head_A_sn <height_A_sn //
- | <unwind2_rmap_S_sn <path_head_S_sn <height_S_sn //
+ #n #_ cases l [ #k ]
+ [ <unwind2_rmap_d_dx <path_head_d_dx <height_d_dx
+ <nplus_comm in ⊢ (??(??%)?); <nplus_assoc
+ >IH -IH <tr_compose_xap <tr_uni_xap_succ //
+ | <unwind2_rmap_m_dx <path_head_m_dx <height_m_dx //
+ | <unwind2_rmap_L_dx <path_head_L_dx <height_L_dx
+ <tr_xap_push <npred_succ <nplus_succ_sn //
+ | <unwind2_rmap_A_dx <path_head_A_dx <height_A_dx //
+ | <unwind2_rmap_S_dx <path_head_S_dx <height_S_dx //