MatchOnIrrelevantData1.agda:17,1-18,43
Cannot split on argument of irrelevant datatype Fin @0
when checking the definition of toNat