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