proposition: Lemma sort_incl : forall B (T S : relation B) l, T << S -> sort T l -> sort S l.
proof: Proof. intros; induction l. intuition. inversion H0. apply cons_sort; intuition. subst. eapply sort_incl_aux; ehyp. Qed.
imports: Coq(List Morphisms Lia) CoLoR(RelUtil LogicUtil)