Set Nested Proofs Allowed.

Class Foo.

Goal True.

Instance foo: Foo.
Qed.

trivial.

Qed.