</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The type of the term <span><strong class="command">t</strong></span> must be an inductive
type or the application of an inductive type.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It proceeds by cases on <span><strong class="command">t</strong></span> paying attention
to the constraints imposed by the actual "right arguments"
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The type of the term <span><strong class="command">t</strong></span> must be an inductive
type or the application of an inductive type.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It proceeds by cases on <span><strong class="command">t</strong></span> paying attention
to the constraints imposed by the actual "right arguments"