theory Test imports Main begin

locale L begin
  coinductive P where "P 0"
  lemma "P n" proof (coinduction rule: P.coinduct)
    case P show ?case sorry (* case P and ?case are recognized *)
  qed
end

lemma "L.P n" proof (coinduction rule: L.P.coinduct)
  case P show ?case sorry (* Undefined case: "P", Unbound schematic variable: ?case *)
qed

end