An example of Thinnings for a very specific use case.

Thinnings.idr

data CanSkip = MustKeep | CanSkip
data ThinnedList : (a : Type)
                -> (contract : List (Pair a CanSkip))
                -> Type
  where
    Empty : ThinnedList a Nil
    Add  : (x : a) 
        -> (rest : ThinnedList a xs) -> ThinnedList a ((x,b      )::xs)
    Skip : (rest : ThinnedList a xs) -> ThinnedList a ((x,CanSkip)::xs)