proposition: Lemma Sorted_rect : forall P:list A -> Type, P [] -> (forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) -> forall l:list A, Sorted l -> P l.
proof: Proof. intros P ? ? l. induction l. - firstorder using Sorted_inv. - firstorder using Sorted_inv. Qed.
imports: List Relations Relations_1