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