Function lemma_disjoint_refined_left 

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

requires

disjoint_domains(refined.0, other),

ensures

#[trigger] disjoint_domains(refined, other),

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