Function lemma_disjoint_mapped_left 

pub broadcast proof fn lemma_disjoint_mapped_left<Inner: SpecParser, M: SpecMapper<In = Inner::PVal>, P: SpecParser>(
    mapped: Mapped<Inner, M>,
    other: P,
)

requires

disjoint_domains(mapped.inner, other),

ensures

#[trigger] disjoint_domains(mapped, other),

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