+
+(* Constructions with path_append *******************************************)
+
+lemma path_head_refl_append (p) (q) (n):
+ q = ↳[n]q → q = ↳[n](p●q).
+#p #q elim q -q
+[ #n #Hn <(eq_inv_path_empty_head … Hn) -Hn //
+| #l #q #IH #n @(nat_ind_succ … n) -n
+ [ #Hq | #n #_ cases l [ #k ] ]
+ [ lapply (eq_inv_path_head_zero_dx … Hq) -Hq #Hq destruct
+ | <path_head_d_dx <path_head_d_dx
+ | <path_head_m_dx <path_head_m_dx
+ | <path_head_L_dx <path_head_L_dx
+ | <path_head_A_dx <path_head_A_dx
+ | <path_head_S_dx <path_head_S_dx
+ ] #Hq
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+ /3 width=1 by eq_f/
+]
+qed-.
+
+(* Inversions with path_append **********************************************)
+
+lemma eq_inv_path_head_refl_append (p) (q) (n):
+ q = ↳[n](p●q) → q = ↳[n]q.
+#p #q elim q -q
+[ #n #Hn <(eq_inv_path_empty_head … Hn) -p //
+| #l #q #IH #n @(nat_ind_succ … n) -n //
+ #n #_ cases l [ #k ]
+ [ <path_head_d_dx <path_head_d_dx
+ | <path_head_m_dx <path_head_m_dx
+ | <path_head_L_dx <path_head_L_dx
+ | <path_head_A_dx <path_head_A_dx
+ | <path_head_S_dx <path_head_S_dx
+ ] #Hq
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+ /3 width=1 by eq_f/
+]
+qed-.