<unwind2_path_L_sn <Hr2 -Hr2 //
| #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
@(ex3_2_intro … s1 (s2●𝗔◗r2)) //
<unwind2_path_L_sn <Hr2 -Hr2 //
| #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
@(ex3_2_intro … s1 (s2●𝗔◗r2)) //