proposition: Lemma sort_transitive : forall B (a : B) L rel, transitive rel -> sort rel (a::L) -> forall x, In x L -> rel a x.
proof: Proof. intros. induction L. destruct H1. simpl in H1; destruct H1. subst. inversion H0; subst; auto. inversion H4; subst; auto. apply IHL; auto. inversion H0; inversion H4. subst. apply cons_sort. subst; auto. inversion H5. subst. inversion H9. apply nil_leA. subst. apply cons_leA. eapply H; eauto. Qed.
imports: Coq(List Morphisms Lia) CoLoR(RelUtil LogicUtil)