TelescopingLet2.agda:4,9-10 Not in scope: ★ at TelescopingLet2.agda:4,9-10 when scope checking ★