TelescopingLet3.agda:15,6-36
let open Star using (★₁) is not allowed in a telescope here.
when scope checking the declaration
  data D3 (let open Star using (★₁)) : ★₁