Function lemma_disjoint_void_left 

pub broadcast proof fn lemma_disjoint_void_left<Other: SpecParser>(void: Void, other: Other)

ensures

#[trigger] disjoint_domains(void, other),

Void accepts no input and is therefore disjoint from every parser.