proposition: Lemma LocallySorted_cons: forall l a b, LocallySorted R (b::l) /\ R a b <-> LocallySorted R (a::b::l).
proof: Proof. Proof with auto. intros l a; split. - destruct l; intros H; destruct H as [Eq S]. + now constructor. + constructor; trivial. - generalize dependent a. destruct l. intros a0 H. + split; auto. now inversion_clear H. now inversion H. + inversion 1. split;auto. Qed.
imports: hydras(DecPreOrder_Instances)