proposition: Theorem isorted2 : forall (x1 x2:A)(l':list A), R x1 x2 -> impredicative_sorted (x2::l') -> impredicative_sorted (x1::x2::l').
proof: Proof. intros x1 x2 l' Hr Hs P Hsn Hs1 Hs2. apply Hs2; auto. apply Hs; auto. Qed.
imports: List Relations