reg032.idr

module reg032

zfin : Fin 1
zfin = 0

data Infer = MkInf a

foo : Infer
foo = MkInf (the (Fin 1) 0)