1 2 3 4 5 6 7 8 9 10 11 12
Set Nested Proofs Allowed. Class Foo. Class Bar := b : Type. Instance foo : Foo. Instance bar : Bar. exact Type. Defined. Defined.