do not use flatterms for discrimination trees (not adapted for big terms rewriting);
use the pre-computed size of terms instead