namedCases : string list -> tactic
STRUCTURE
SYNOPSIS
Case split on type of leading universally quantified variable in the goal, using given names for introduced constructor arguments.
DESCRIPTION
bossLib.namedCases is identical to BasicProvers.namedCases.
SEEALSO
HOL  Trindemossen-1