Function lemma_disjoint_symmetric 

pub proof fn lemma_disjoint_symmetric<Left: SpecParser, Right: SpecParser>(
    left: Left,
    right: Right,
)

requires

disjoint_domains(left, right),

ensures

disjoint_domains(right, left),

Disjointness is symmetric, but symmetry is deliberately not broadcast: broadcasting it creates a quantifier-instantiation cycle with every directional decomposition rule below.