+lemma path_head_structure_height (p) (m):
+ ⊗↳[m]p = ↳[m+♯↳[m]p]⊗p.
+#p elim p -p //
+#l #p #IH #m @(nat_ind_succ … m) -m //
+#m #_ cases l [ #n ]
+[ <height_d_sn <structure_d_sn //
+| <structure_m_sn //
+| <structure_L_sn //
+| <height_A_sn <structure_A_sn <nplus_succ_sn <path_head_A_sn //
+| <height_S_sn <structure_S_sn <nplus_succ_sn <path_head_S_sn //