Function lemma_disjoint_tuple_2 

pub broadcast proof fn lemma_disjoint_tuple_2<A: SpecParser, B: SpecParser, C: SpecParser, D: SpecParser>(
    t1: Pair<A, B>,
    t2: Pair<C, D>,
)

requires

forall |input: Seq<u8>| (
    #[trigger]
    t1
        .0
        .spec_parse(
            input,
        ) matches Some(
        (n1, _),
    ) ==> t2.0.spec_parse(input) matches Some((n2, _)) ==> n1 == n2
),

disjoint_domains(t1.1, t2.1),

ensures

#[trigger] disjoint_domains(t1, t2),

Two tuples are disjoint if their first parsers consume equal bytes and their second parsers are disjoint.