TelescopingLet1.agda:6,10-11
Not in scope:
  ★ at TelescopingLet1.agda:6,10-11
when scope checking ★