Non inductive definition of sorted lists

Here are two definitions of sorted lists. Prove that they are equivalent.

Require Export List.

Inductive sorted (A:Set)(R:A->A->Prop) : list A -> Prop :=
  | sorted0 : sorted A R nil
  | sorted1 : forall x:A, sorted A R (cons x nil)
  | sorted2 :
      forall (x y:A)(l:list A),
        R x y ->
        sorted A R (cons y l)-> sorted A R (cons x (cons y l)).

Definition sorted' (A:Set)(R:A->A->Prop)(l:list A) :=
  forall (l1 l2:list A)(n1 n2:A),
    l = app l1 (cons n1 (cons n2 l2))-> R n1 n2.

Solution