Function lemma_disjoint_bind_left 

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

requires

disjoint_domains(bind.0, other),

ensures

#[trigger] disjoint_domains(bind, other),

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