Function lemma_disjoint_named_left 

pub broadcast proof fn lemma_disjoint_named_left<Inner: SpecParser, Other: SpecParser>(
    named: Named<Inner>,
    other: Other,
)

requires

disjoint_domains(named.1, other),

ensures

#[trigger] disjoint_domains(named, other),

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