Function lemma_disjoint_choice 

pub broadcast proof fn lemma_disjoint_choice<S1: SpecParser, S2: SpecParser, S3: SpecParser>(
    choice: Choice<S1, S2>,
    other: S3,
)

requires

disjoint_domains(other, choice.0),

disjoint_domains(other, choice.1),

ensures

#[trigger] disjoint_domains(other, choice),

A Choice parser is disjoint from another parser if both branches are.

NOTE

The trigger disjoint_domains(other, choice) matches Choice(..., Choice(..., ...)) but not Choice(Choice(..., ...), ...).