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