IrrelevantFamilyIndex.err

IrrelevantFamilyIndex.agda:26,3-11
Failed to infer the value of dotted pattern
when checking that the pattern .(suc n) has type Nat