This makes the identifying information be of type bset*bset instead of
bset and adds tracking of deferrals for propositional reasoning and --
in case of K -- for modal reasoning