- | <path_head_m_sn <list_append_lcons_sn #Hp
- elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
- <reverse_lcons <lift_rmap_m_dx /2 width=1 by/
- | <path_head_L_sn <list_append_lcons_sn #Hp
- elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
- <reverse_lcons <lift_rmap_L_dx <nplus_succ_sn /2 width=1 by/
- | <path_head_A_sn <list_append_lcons_sn #Hp
- elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
- <reverse_lcons <lift_rmap_A_dx /2 width=2 by/
- | <path_head_S_sn <list_append_lcons_sn #Hp
- elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
- <reverse_lcons <lift_rmap_S_dx /2 width=2 by/
+ | <path_head_m_dx #Hq
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+ <lift_rmap_m_dx /2 width=1 by/
+ | <path_head_L_dx #Hq
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+ <lift_rmap_L_dx <nplus_succ_sn /2 width=1 by/
+ | <path_head_A_dx #Hq
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+ <lift_rmap_A_dx /2 width=2 by/
+ | <path_head_S_dx #Hq
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+ <lift_rmap_S_dx /2 width=2 by/