Data.Type.Fin.Indexed

data IFin

class LessEq x y

ifinZ

weaken

ifinNat

ifinVal

onIFinPred