Goal "!t e. normal(normif b t e) = (normal t & normal e)";