proposition: Lemma LocallySorted_cons' (Htrans : Transitive R): forall l a, List.Forall (R a) l /\ LocallySorted R l <-> LocallySorted R (a::l).
proof: Proof. Proof with auto. induction l. - split. + constructor. + split; constructor. - split. + intros;apply LocallySorted_cons. split. * now destruct H. * destruct H as [H _]. now inversion H. + inversion 1;split;auto. constructor. * auto. * rewrite <- IHl in H2. destruct H2. apply forall_weak with a;auto. Qed.
imports: hydras(DecPreOrder_Instances)