proposition: Lemma Sorted_extends : Transitive R -> forall a l, Sorted (a::l) -> Forall (R a) l.
proof: Proof. intros H a l H0. change match a :: l with [] => True | a :: l => Forall (R a) l end. induction H0 as [|? ? ? ? H1]; [trivial|]. destruct H1; constructor; trivial. eapply Forall_impl; [|eassumption]. firstorder. Qed.
imports: List Relations Relations_1