Function lemma_disjoint_eof 

pub broadcast proof fn lemma_disjoint_eof<P: Productive>(p: P, eof: Eof)

requires

p.productive_inv(),

p.safe_inv(),

ensures

#[trigger] disjoint_domains(p, eof),

A productive parser is disjoint from Eof.