Function lemma_disjoint_bimap_left 

pub broadcast proof fn lemma_disjoint_bimap_left<Inner: SpecParser, M: SpecMap<Input = Inner::PVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>, P: SpecParser>(
    mapped: Mapped<Inner, BiMap<M, MRev>>,
    other: P,
)

requires

disjoint_domains(mapped.inner, other),

ensures

#[trigger] disjoint_domains(mapped, other),

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