proposition: Lemma raw_equal_eq : forall a (Ha: Sorted (Raw.ltk key_ord) a) b (Hb: Sorted (Raw.ltk key_ord) b), Raw.equal key_comp cmp a b = true -> a = b.
proof: Proof. induction a; intros. simpl in H. case b in *; auto. now contradict H. destruct a as (xa, ea). simpl in H. case b in *. now contradict H. destruct p as (xb, eb). destruct (compare xa xb); auto; try (now contradict H). rewrite andb_true_iff in H. destruct H. unfold cmp in H. destruct (compare ea eb); auto; try (now contradict H). subst. apply f_equal. apply IHa; auto. now inversion Ha. now inversion Hb. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance