proposition: Lemma list_app_last : forall l m n (a : A), l ++ m = n ++ a::nil -> m <> nil -> In a m.
proof: Proof. intros l m n; revert l m; induction n; simpl; intros. destruct l. simpl in H; rewrite H; auto with datatypes. inversion H. absurd (m = nil); trivial. apply (proj2 (app_eq_nil l m H3)). destruct l. simpl in H; rewrite H; auto with datatypes. inversion H. apply IHn with l; trivial. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)