proposition: Lemma equal_cons : forall cmp l1 l2 x y, Ok (x::l1) -> Ok (y::l2) -> eqk x y -> cmp (snd x) (snd y) = true -> (Equivb cmp l1 l2 <-> Equivb cmp (x :: l1) (y :: l2)).
proof: Proof. intros. inversion H; subst. inversion H0; subst. destruct x; destruct y; compute in H1, H2. split; intros. apply equal_2; auto. simpl. case X.compare_spec; intros; try MX.order. rewrite H2; simpl. apply equal_1; auto. apply equal_2; auto. generalize (equal_1 H3). simpl. case X.compare_spec; try discriminate. rewrite andb_true_iff. intuition. Qed.
imports: Coq(OrdersFacts OrdersLists)