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.