proposition: Lemma list_app_eq_simpl2 (a : A) (l l0 l' l0' : list A) : l ++ a :: l' = l0 ++ l0' -> length l < length l0 -> exists lr, l0 = l ++ a :: lr /\ l' = lr ++ l0'.
proof: Proof. change (l ++ a :: l') with (l ++ (a :: nil) ++ l'); intros. rewrite app_assoc in H; apply list_app_eq_simpl in H; desf. by exists lr; rewrite <- app_assoc. rewrite length_app; ins; lia. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt