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.