<h4>Inductive Type Definitions</h4><p>Inductive types are specified by introduction rules. Each introduction rule is specified in <a href="induction/ConstructorShape.html" name="provingground.induction.ConstructorShape" id="provingground.induction.ConstructorShape" class="extype">ConstructorShape</a> (without specifying the type)
and <a href="induction/ConstructorTL.html" name="provingground.induction.ConstructorTL" id="provingground.induction.ConstructorTL" class="extype">ConstructorTL</a> including the sp