Function lemma_disjoint_repeat 

pub broadcast proof fn lemma_disjoint_repeat<P: SpecParser, A: SpecParser, B: SpecParser>(
    p: P,
    repeat: Repeat<A, B>,
)

requires

disjoint_domains(p, repeat.0),

disjoint_domains(p, repeat.1),

ensures

#[trigger] disjoint_domains(p, repeat),

A Repeat<A, B> parser is disjoint from another parser if both A and B are.