Function lemma_disjoint_terminated 

pub broadcast proof fn lemma_disjoint_terminated<U: SpecParser, U1: SpecParser, V1: SpecParser, const CHECK: bool>(
    p: U,
    p1: Terminated<U1, V1, V1::PVal, CHECK>,
)

requires

disjoint_domains(p, p1.a),

ensures

#[trigger] disjoint_domains(p, p1),

A Terminated parser is disjoint from another parser if its prefix is.