The reference, in prose, asserts that the tree is pairwise disjoint at each
level but I don't see this reflected in the axioms or FOL. Apologies if I've
missed it. In that section there is also a statement of universal
exhaustiveness, though I think in conversations we have left some (all?)
sibling sets as not mutually exhaustive.
Original issue reported on code.google.com by alanruttenberg@gmail.com on 8 May 2012 at 1:49
Original issue reported on code.google.com by
alanruttenberg@gmail.comon 8 May 2012 at 1:49