proposition: Lemma LocallySorted_inv_In (Htrans : Transitive R): forall l x, LocallySorted R (x::l) -> forall y, In y l -> R x y.
proof: Proof. induction l. - inversion 2. - intros x H y H0; case (in_inv H0). + intro;subst y;inversion_clear H;auto. + intros; eapply IHl;auto. inversion H; apply LocallySorted_trans with a;auto. Qed.
imports: hydras(DecPreOrder_Instances)