Post #1942215

@mevenlennonbertrand i think i had a similar realisation recently when i saw someone motivate the subformula property by saying "we don't have to guess anything in proof search". it really is not at all about subformulas and all about information flow...