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