proposition: Lemma truncate_same: forall (s : stack A), truncate (length s) s = s.
proof: Proof. intros. unfold truncate. destruct s. destruct Nat.compare;trivial. rewrite nat_compare_n_n. trivial. Qed.
imports: Coq(List) Coq(Arith)