Data.List.Sufficient

WellFounded on List suffixes

Definitions

data Suffix : List a -> List a -> Type

Totality: total
Visibility: public export
Constructor: 

IsSuffix : (x : a) -> (zs : List a) -> (0 _ : xs = x :: (zs ++ ys)) -> Suffix ys xs

Hint: 

WellFounded (List a) Suffix