Function lemma_disjoint_implicit 

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

requires

disjoint_domains(other, implicit.0),

ensures

#[trigger] disjoint_domains(other, implicit),

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