Function lemma_disjoint_tuple 

pub broadcast proof fn lemma_disjoint_tuple<U: SpecParser, U1: SpecParser, V1: SpecParser>(
    t: U,
    t1: Pair<U1, V1>,
)

requires

disjoint_domains(t, t1.0),

ensures

#[trigger] disjoint_domains(t, t1),

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