My code works this way. Proofs are serialization of a subset of the tree, and to validate a proof you ask a single function whether a particular value is included in that tree subset, and it answers yes or no, so obviously it's impossible for a single value to both validate and not validate. The proof code was quite terrifying before I made this change (which I did on your suggestion), and it's much cleaner and simpler now. It also in principle supports compact proofs of multiple inclusions and exclusions in the same serialization of a subset of the tree because the upper branches won't have to be repeated. I haven't written code for generating those, but the validation code will happily accept them.

I'm not sure what you mean by MMRs though. Are you talking about MMRs where each mountain is a set of diffs to the old things and are periodically consolidated? Or do later mountains refer to internals of earlier ones? Or do they have 'maybe' values which mean that the earlier mountain should be referred to? Are these patricia tries or something flatter and more fixed depth?

My code doesn't keep track of tree size, by the way. It would be trivial to add that functionality to the library, and including it in the hashing creates complexity and doesn't seem to have any benefit over sending that data in a side channel.