Cases : tactic
STRUCTURE
SYNOPSIS
Case split on leading universally quantified variable in a goal.
DESCRIPTION
bossLib.Cases is identical to BasicProof.Cases.
SEEALSO
HOL  Kananaskis-13