canonical 'cases'/'induct' rules for n-tuples (n=3..7)
(really belongs to theory Product_Type, but doesn't work there yet)
Ifexpr.thy: prolog boolex value ifex valif bool2if normif norm normal end
cat prolog boolex value ifex valif bool2if normif norm normal end > Ifexpr.thy