Improving efficiency of normalize_EXT

[QinshiWang]

The tactic normalize_EXT is used to flatten extern predicates. For example, after unfolding an extern predicate, we have

(EXT
   [ExtPred.and
      (FilterRepr.filter_repr p index_w panes rows cf)
      (ExtPred.prop
         (filter_sim H_num_slots H_num_rows hashes
            tick_time f cf))])))

We get

(EXT
   [FilterRepr.filter_repr p index_w panes rows cf;
   ExtPred.prop
     (filter_sim H_num_slots H_num_rows hashes tick_time f
        cf)]))) Filter_fd []

after normalize_EXT.
But normalize_EXT is slow now. We want to optimize it, maybe just by taking out the part to rewrite to avoid rewriting cost proportion to the size of the whole goal.