proposition: Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 -> CompSpec eq lt l1 l2 c -> CompSpec eq lt (x1::l1) (x2::l2) c.
proof: Proof. destruct c; simpl; inversion_clear 2; auto with relations. Qed.
imports: Bool SetoidList RelationClasses Morphisms RelationPairs Equalities Orders OrdersFacts