Function lemma_disjoint_implicit_left 

pub broadcast proof fn lemma_disjoint_implicit_left<Head: SpecParser, Tail: DepCombinator<Key = Head::PVal>, U: SpecParser>(
    implicit: Implicit<Head, Tail>,
    other: U,
)
where
    Tail::Body: SpecParser<PVal = Tail::Val>,

requires

disjoint_domains(implicit.0, other),

ensures

#[trigger] disjoint_domains(implicit, other),

An implicit dependent parser is disjoint from another parser if its head parser is.