proposition: Lemma equal_1 : forall m m', Equivb m m' -> equal m m' = true.
proof: Proof. intros m m'; apply Raw.equal_1; auto. apply m.(sorted). apply m'.(sorted). Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses