fact: Definition impredicative_sorted (l:list A) : Prop := forall P : list A -> Prop, P nil -> (forall x:A, P (x::nil))-> (forall (x1 x2:A)(l':list A), R x1 x2 -> P (x2::l') -> P (x1::x2::l'))-> P l.
imports: List Relations