Function lemma_disjoint_mapped 

pub broadcast proof fn lemma_disjoint_mapped<P: SpecParser, Inner1: SpecParser, M1: SpecMapper<In = Inner1::PVal>>(
    p: P,
    m: Mapped<Inner1, M1>,
)

requires

disjoint_domains(p, m.inner),

ensures

#[trigger] disjoint_domains(p, m),

A Mapped parser is disjoint from another parser if its inner parser is.