Function lemma_disjoint_alt_left 

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

requires

disjoint_domains(alt.0, other),

disjoint_domains(alt.1, other),

ensures

#[trigger] disjoint_domains(alt, other),

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