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 as [ |a a0 IHa]; intros Ha b Hb H. - 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 as [H H0]. unfold cmp in H. rewrite compare2eqb_spec in H. subst. apply f_equal. apply IHa; auto. * now inversion Ha. * now inversion Hb. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance