proposition: Lemma list_drop_last : forall l m n (a : A), l ++ m = n ++ a::nil -> m <> nil -> exists2 w, w [= m & l ++ w = n.
proof: Proof. induction l; intros. simpl in H. exists n. rewrite H; auto with datatypes. auto. destruct n. simpl in H. destruct (app_eq_unit (a::l) m H) as [[l_nil r_unit] | [l_unit r_nil]]; try contr. discr. inversion H. destruct (IHl m n a0); trivial. exists x; trivial. rewrite <- H4. auto with datatypes. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)