proposition: Lemma Sorted_LocallySorted_iff : forall l, Sorted l <-> LocallySorted l.
proof: Proof. split; [induction 1 as [|a l [|]]| induction 1]; auto using Sorted, LocallySorted, HdRel. match goal with H1 : HdRel a (_ :: _) |- _ => inversion H1 end. subst; auto using LocallySorted. Qed.
imports: List Relations Relations_1