disable sorry check when using previous exercises

[robertylewis]

Some assignments are expected to be structured like this:

@[autogradedProof 1] theorem aLemma : SomeProp := sorry 

@[autogradedProof 1] theorem mainResult : SomeOtherProp := sorry 
/- this proof uses `aLemma` -/

If a student proves mainResult dependent on aLemma, but doesn't prove aLemma, they won't get points on either.

We should add an option that stops the sorry check from recursing into declarations that are themselves tagged as autograded, so that the right amount of partial credit gets assigned here.