proposition: Lemma sorted'2 : forall x y l, R x y -> sorted' (y :: l)-> sorted' (x :: y :: l).
proof: Proof. intros x y l Hr Hs l1; case l1. - intros l2 n1 n2 Heq; injection Heq; intros; subst; trivial. - simpl; intros a l1' l2 n1 n2 Heq; injection Heq. intros Heq' Heqx; apply (Hs l1' l2); trivial. Qed.
imports: List Relations