Data.Extensible.Internal

data Position xs x

runPosition

comparePosition

data Nav xs x

navigate

here

navL

navR

class Member xs x

type x ∈ xs

data Nat

class Record n

type family Lookup x xs :: Nat

type family Succ x :: Nat

type family Half xs :: [k]

type family Tail xs :: [k]

lemmaHalfTail