repeat (first | apply IsQuizSchema.consQuiz (by decide)
              | apply IsQuizSchema.consNonQuiz (by decide)
              | apply IsQuizSchema.nil)
η : Type u_η
inst✝ : DecidableEq η
sch : Schema
⊢ IsQuizSchema (schema gradebook)
no goals