Function lemma_disjoint_bimap 

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

requires

disjoint_domains(other, mapped.inner),

ensures

#[trigger] disjoint_domains(other, mapped),

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