No index entry for `model_check` tactic

[bkushigian]

I'm not seeing an index entry for the model_check tactic. This is conceptually a simple enough tactic that it probably doesn't matter, but mentioning it in case this was an oversight.

[achlipala]

Yeah, that connects to an interesting didactic question. The tactics documented in that index are meant to be used throughout the book, whereas recommended use of model_check is concentrated narrowly -- it's really meant mostly as a supplement to certain chapters. I also think it would need significantly more documentation than the other tactics, depending more on definitions from the book library, etc., so I think I'll hold off on adding an entry for now.