Function lemma_disjoint_ref_right 

pub broadcast proof fn lemma_disjoint_ref_right<Other: SpecParser, Inner: SpecParser>(
    other: Other,
    borrowed: Ref<Inner>,
)

requires

disjoint_domains(other, borrowed.0),

ensures

#[trigger] disjoint_domains(other, borrowed),

Borrowing adaptation does not change a parser’s accepted byte domain.