Function lemma_disjoint_eof_left 

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

requires

p.productive_inv(),

p.safe_inv(),

ensures

#[trigger] disjoint_domains(eof, p),

Eof is disjoint from a productive parser.