Function lemma_disjoint_refined 

pub broadcast proof fn lemma_disjoint_refined<Inner: SpecParser, P1: SpecPred<Inner::PVal>, P2: SpecPred<Inner::PVal>>(
    r1: Refined<Inner, P1>,
    r2: Refined<Inner, P2>,
)

requires

r1.0 == r2.0,

forall |v: Inner::PVal| r1.1.apply(v) ==> !r2.1.apply(v),

ensures

#[trigger] disjoint_domains(r1, r2),

Two Refined parsers with the same inner parser and mutually exclusive predicates are disjoint.