Function lemma_disjoint_alt 

pub broadcast proof fn lemma_disjoint_alt<S1: SpecParser, S2: SpecParser<PVal = S1::PVal>, S3: SpecParser<PVal = S1::PVal>>(
    alt: Alt<S1, S2>,
    other: S3,
)

requires

disjoint_domains(other, alt.0),

disjoint_domains(other, alt.1),

ensures

#[trigger] disjoint_domains(other, alt),

An Alt parser is disjoint from another parser if both branches are.

NOTE

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