Data.Type.Fin

data Fin

elimFin

fins

fin

finZ

weaken

without

finNat