Function lemma_disjoint_const_refined 

pub broadcast proof fn lemma_disjoint_const_refined<Inner: SpecParser, P: SpecPred<Inner::PVal>>(
    tag: Const<Inner, Inner::PVal>,
    r: Refined<Inner, P>,
)

requires

tag.0 == r.0,

!r.1.apply(tag.1),

ensures

#[trigger] disjoint_domains(tag, r),

A Const parser is disjoint from a Refined parser with the same inner parser if the refined predicate does not hold on the const value.