proposition: Lemma force_split : forall A h' ls' (x : A) h ls, h ++ h' = ls ++ x :: ls' -> ~In x h' -> exists ls'', h = ls ++ x :: ls''.
proof: Proof. induction h; simpl; intuition subst. exfalso; apply H0. apply in_or_app; simpl; eauto. destruct ls; simpl in *. injection H; intros; subst; eauto. injection H; clear H; intros; subst. apply IHh in H; auto. firstorder. eexists; f_equal; eauto. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)