proposition: Lemma level_1: forall (s s' t t' : stack A), (s', t') = level s t -> length s' = length t'.
proof: Proof. intros. unfold level in H. case_eq (Nat.compare (length s) (length t));intros;rewrite H0 in H. apply nat_compare_Eq in H0. inversion H. trivial. inversion H;subst. apply truncate_1. apply nat_compare_lt in H0. auto with *. inversion H;subst. symmetry. apply truncate_1. apply nat_compare_gt in H0. auto with *. Qed.
imports: Coq(List) Coq(Arith)