proposition: Lemma sort_incl_aux : forall B (T S : relation B) a l, T << S -> lelistA T a l -> lelistA S a l.
proof: Proof. induction l; intros. intuition. destruct H0; intuition. Qed.
imports: Coq(List Morphisms Lia) CoLoR(RelUtil LogicUtil)