1 consts norm :: ifex => ifex
2 primrec
3 "norm (CIF b) = CIF b"
4 "norm (VIF x) = VIF x"
5 "norm (IF b t e) = normif b (norm t) (norm e)"