proposition: Lemma prec_split : forall A h (l : A) x l' x0 l'' x1, h ++ [l] = x ++ l' :: x0 ++ l'' :: x1 -> (x1 = nil /\ l = l'' /\ h = x ++ l' :: x0) \/ exists x1', x1 = x1' ++ [l] /\ h = x ++ l' :: x0 ++ l'' :: x1'.
proof: Proof. destruct x1; t. rewrite app_comm_cons in *. rewrite app_assoc in H. apply app_inj_tail in H; t. specialize (@exists_last _ (a :: x1)). t. firstorder (try congruence). rewrite p in H. repeat (rewrite app_comm_cons in * || rewrite app_assoc in *). apply app_inj_tail in H; t. rewrite <- app_assoc. simpl; eauto. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)