Clarification on guarded conjunction ("Dynamic")
I forgot to distinguish this sort of conjunction from the conjunction that "and" implements. It's really not the same thing.
Simple conjunction can't do this right. Simple conjunction is built from 2 decompositions of $1. But there's no reasonable way to decompose the half-box in which the guard fails. Doing so would mean that the type-incorrect subformula was used despite being type-incorrect.
Instead, these guarded conjunctions are headed by
(guard (accepts-type X Y) (X Y))
It decomposes like this. Note that one cannot further decompose the half-box where the guard fails.