proposition: Lemma truncate_nil: forall (s : stack A), truncate 0 s = nil.
proof: Proof. intros. induction s. unfold truncate. unfold Nat.compare; trivial. unfold truncate. replace (Nat.compare 0 (length (a::s))) with Lt by trivial. trivial. Qed.
imports: Coq(List) Coq(Arith)