Cases

BasicProvers.Cases : tactic

Case split on leading universally quantified variable in a goal.

bossLib.Cases is identical to BasicProof.Cases.

See also

bossLib.Cases