This avoids the proofmode to be irritated by unrelated goals with a typeclass type.
Attach a file by drag & drop or click to upload
Ralf Jung authored