Function lemma_disjoint_refined_right 

pub broadcast proof fn lemma_disjoint_refined_right<Other: SpecParser, Inner: SpecParser, Pred: SpecPred<Inner::PVal>>(
    other: Other,
    refined: Refined<Inner, Pred>,
)

requires

disjoint_domains(other, refined.0),

ensures

#[trigger] disjoint_domains(other, refined),

Refining the right parser can only narrow its accepted byte domain.