proposition: Lemma eq_cons : forall l1 l2 x y, O.eq x y -> eq l1 l2 -> eq (x :: l1) (y :: l2).
proof: Proof. unfold eq; intros l1 l2 x y Exy E12 z. split; inversion_clear 1. - left; MO.order. - right; rewrite <- E12; auto. - left; MO.order. - right; rewrite E12; auto. Qed.
imports: Bool SetoidList RelationClasses Morphisms RelationPairs Equalities Orders OrdersFacts