Cases_on can be used to specify variables that are buried in the quantifier prefix. Cases_on can also be used to perform case splits on non-variable terms. If M is a non-variable term that does not occur bound in the goal, then the cases theorem is instantiated with M and used to generate as many sub-goals as there are disjuncts in the cases theorem.