The transitive closure puzzle

TransitiveClosure.idr

module TransitiveClosure

data Index : (xs : List a) -> Type where
  Z : Index (x :: xs)
  S : Index xs -> Index (x :: xs)

Uninhabited (Index []) where
  uninhabited (Z) impossible
  uninhabited (S _) impossible

nth : {list:List a} -> Index list -> a
nth {list = []} Z impossible
nth {list = []} (S _) impossible
nth {list = (a :: _)} Z = a
nth {list = (_ :: xs)} (S x) = nth {list=xs} x

data Trans : (a -> a -> Type) -> a -> a -> Type where
  Straight : p a b -> Trans p a b
  Indirect : Trans p a b -> p b c -> Trans p a c

contains : a -> List a -> Type
contains item set = (i:Index set ** nth i=item)

data Every : (a -> Type) -> Type where
  Each : (s:List a)
    -> ((item : a) -> contains item s -> p item)
    -> ((item : a) -> p item -> contains item s)
    -> Every p

-- The goal is here:
transitive_closure : DecEq s => (g:List s) -> (p:Index g -> s -> s -> Type)
  -> ((i:Index g) -> (x:s) -> (y:s) -> Dec (p i x y))
  -> (x:s) -> Every (Trans (\x, y => (i:Index g ** (p i x y))) x)