Any-comm : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
           Any P (xs ++ ys) → Any P (ys ++ xs)
Any-comm xs [] prf = {!!}

Goal: Any P xs
————————————————————————————————————————————————————————————
prf : Any P (xs ++ [])
xs  : List A
P   : A → Set  (not in scope)
A   : Set  (not in scope)