Induct : tactic
STRUCTURE
SYNOPSIS
Induct on leading universally quantified variable in a goal.
DESCRIPTION
bossLib.Induct is identical to BasicProvers.Induct.
SEEALSO
HOL  Trindemossen-1