proposition: Lemma sorted'_imp_sorted: forall l, sorted' l -> sorted l.
proof: Proof. induction l as [|a l']; auto. - destruct l'; auto. + intro H; constructor. * apply (H nil l'); auto. * apply IHl'; apply (sorted'_inv _ _ H). Qed.
imports: List Relations