proposition: Lemma LocallySorted_trans (Htrans : Transitive R): forall l a x, LocallySorted R (a::l) -> R x a -> LocallySorted R (x::l).
proof: Proof. inversion_clear 1. - constructor. - intro; refine (LSorted_consn x H0 _). + now transitivity a. Qed.
imports: hydras(DecPreOrder_Instances)