IN COQ PLEASE Create an inductive relation that holds if, and only if, element 'x' appears before element 'y' in the given list. We can define `succ` inductively as follows: (x, y) succ l -----------------------R1 ------------------R2 (x, y) succ x :: y :: l (x, y) succ z :: l Rule R1 says that x succeeds y in the list that starts with [x, y]. Rule R2 says that if x succeeds y in list l then x succeeds y in a list the list that results from adding z to list l. ======================================================================== Like this: Inductive succ {X : Type} (x:X) (y:X): list X -> Prop :=