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