proposition: Lemma nil_cons_end: forall (T: Type)(l: list T)(e: T), not((l++[e]) = nil).
proof: Proof. intros. intro. destruct l. rewrite app_nil_l in H. assert (A := @nil_cons T e nil). symmetry in H. apply A in H. assumption. rewrite <- app_comm_cons in H. assert (A := @nil_cons T t (l ++ [e])). symmetry in H. apply A in H. assumption. Qed.
imports: Coq(Bool Arith Arith.Peano_dec Arith.Compare_dec List)