proposition: Lemma equal_2 : forall m m', equal m m' = true -> Equivb m m'.
proof: Proof. intros m m'; unfold Equivb, equal. case (eq_dec (default m) (default m')); intros. - split; auto. apply Raw.equal_2 in H; auto. apply m.(sorted). apply m'.(sorted). - now contradict H. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance