Function lemma_disjoint_ref_left 

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

requires

disjoint_domains(borrowed.0, other),

ensures

#[trigger] disjoint_domains(borrowed, other),

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