proposition: Lemma equal_cons : forall cmp l1 l2 x y, Sort (x::l1) -> Sort (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 (compare k k0); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH). rewrite H2; simpl. apply equal_1; auto. apply equal_2; auto. generalize (equal_1 H H0 H3). simpl. case (compare k k0); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH). rewrite H2; simpl; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses