proposition: Lemma map_truncate: forall (f : A -> B) n (s : stack A), map f (truncate n s) = truncate n (map f s).
proof: Proof. intros. induction s. unfold truncate in |- *. simpl in |- *. unfold map in |- *. destruct Nat.compare; trivial. unfold truncate in |- *. case_eq (Nat.compare n (length (map f (a :: s)))); intro. generalize H; intro. rewrite map_length in H0. unfold map at 2 in |- *. unfold map in H. rewrite H in |- *. rewrite H0 in |- *. trivial. generalize H; intro. rewrite map_length in H0. unfold map at 2 in |- *. unfold map in H. rewrite H in |- *. rewrite H0 in |- *. assumption. generalize H; intro. rewrite map_length in H0. unfold map at 2 in |- *. unfold map in H. rewrite H in |- *. rewrite H0 in |- *. trivial. Qed.
imports: Coq(List) Coq(Arith)