Agda.TypeChecking.Injectivity
headSymbol
checkInjectivity
functionInverse
data InvView
data MaybeAbort
useInjectivity