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