Function lemma_disjoint_tuple_left 

pub broadcast proof fn lemma_disjoint_tuple_left<U1: SpecParser, V1: SpecParser, U: SpecParser>(
    tuple: Pair<U1, V1>,
    other: U,
)

requires

disjoint_domains(tuple.0, other),

ensures

#[trigger] disjoint_domains(tuple, other),

A tuple parser is disjoint from another parser if its first component is.