Function lemma_disjoint_bind 

pub broadcast proof fn lemma_disjoint_bind<U: SpecParser, Head: SpecParser, Tail: SpecMap<Input = Head::PVal>>(
    other: U,
    bind: Bind<Head, Tail>,
)
where
    Tail::Output: SpecParser,

requires

disjoint_domains(other, bind.0),

ensures

#[trigger] disjoint_domains(other, bind),

A dependent tuple is disjoint from another parser if its head parser is.