Function lemma_disjoint_choices 

pub broadcast proof fn lemma_disjoint_choices<A: SpecParser, B: SpecParser, C: SpecParser, D: SpecParser>(
    left: Choice<A, B>,
    right: Choice<C, D>,
)

requires

disjoint_domains(left.0, right.0),

disjoint_domains(left.0, right.1),

disjoint_domains(left.1, right.0),

disjoint_domains(left.1, right.1),

ensures

#[trigger] disjoint_domains(left, right),

Two balanced Choice trees are disjoint if every cross-branch pair is disjoint.

Unlike composing the two directional decomposition rules, this rule strictly reduces both visible choice constructors and therefore does not introduce a trigger cycle.