@@ -0,0 +1,4 @@
import InductiveVerification
def main : IO Unit :=
IO.println s!"Hello, {hello}!"
The note is not visible to the blocked user.