Function lemma_disjoint_repeat_till_end 

pub broadcast proof fn lemma_disjoint_repeat_till_end<P: Productive, A: SpecParser>(
    p: P,
    repeat: RepeatTillEnd<A>,
)

requires

p.productive_inv(),

p.safe_inv(),

disjoint_domains(p, repeat.0),

ensures

#[trigger] disjoint_domains(p, repeat),

A RepeatTillEnd<A> parser is disjoint from another parser if its inner parser is

• productive and safe, and
• disjoint from the other parser.