Definition opaque {A} (x: A): A.
Proof.
exact x.
Qed.

Then elsewhere define

Definition unknown = opaque (fun n: nat => n).

So you don’t really even need tactics or notations to cleanup the trick.

There’s some tricky weirdness with the trick though.

I think it doesn’t really work with strict prop or homotopy type theory stuff. Extensional type theory makes id equivalent to unit right?

Definition opaque: unit.
Proof.
exact tt.
Qed.

Definition unknown: nat -> nat :=
match opaque with
| _ => fun n => n
end.

Is a similar way of doing the same thing. But you can prove all units are the same so it doesn’t quite work. You can stack on top of this private inductive types devilry?

#[private]
Variant fence: Set := post.
Definition opaque: fence.
Proof.
exact post.
Qed.
Definition unknown: nat -> nat :=
match opaque with
| _ => fun n => n
end.