proposition: Lemma eq_1 : forall m m', Equivb m m' -> eq m m'.
proof: Proof. intros. generalize (@equal_1 m m'). generalize (@eq_equal m m'). intuition. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses