Function lemma_disjoint_repeat_left 

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

requires

disjoint_domains(repeat.0, p),

disjoint_domains(repeat.1, p),

ensures

#[trigger] disjoint_domains(repeat, p),

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