me="provingground.induction.ConstructorSeqMap" id="provingground.induction.ConstructorSeqMap" class="extype">ConstructorSeqMap</a> that have recursive definition of the recursion and induction functions, the former for the case of a
single introduction rule. Traits <a href="ConstructorSeqMapper.html" name="provingground.induction.ConstructorSeqMapper" id="provingground.induction.ConstructorSeqMapper" class="extype">ConstructorSeqMapper</a> and <a href="ConstructorPatternMapper.html" name="provingground.indu