proposition: Lemma list_end : forall (T: Type)(l: list T), l = nil \/ exists l' e, l = l' ++ [e].
proof: Proof. intros. destruct l. left. reflexivity. right. assert (A1 := @nil_cons T t l). apply not_eq_sym in A1. assert (A2 := @exists_last T (t :: l) A1). destruct A2. destruct s. exists x. exists x0. assumption. Qed.
imports: Coq(Bool Arith Arith.Peano_dec Arith.Compare_dec List)