My mind is mush from thinking about coverage checking + HLF. I think I can argue for it being a good idea to try to think about explicit coverage witnesses (i.e. little trees saying where to split) because
(1) It saves me from having to think about the heuristics by which Twelf chooses to split
(2) It's probably a good thing to work out anyway. I think everyone agrees the above heuristics ought to be spitting out witnesses that are independently checked, but this doesn't seem to have been done yet, except perhaps in the sense in which Delphin does it.