Function lemma_preceded_spec_parse_congruence 

pub proof fn lemma_preceded_spec_parse_congruence<const CHECK: bool, A1: SpecParser<PVal = AVal>, A2: SpecParser<PVal = AVal>, B1: SpecParser, B2: SpecParser<PVal = B1::PVal>, AVal>(
    a1: A1,
    a2: A2,
    b1: B1,
    b2: B2,
    a_val: AVal,
)

requires

forall |x: Seq<u8>| #[trigger] a1.spec_parse(x) == a2.spec_parse(x),

forall |x: Seq<u8>| #[trigger] b1.spec_parse(x) == b2.spec_parse(x),

ensures

forall |x: Seq<u8>| {
    #[trigger]
    (Preceded::<A1, AVal, B1, CHECK> {
        a: a1,
        b: b1,
        a_val,
    })
        .spec_parse(x)
        == (Preceded::<A2, AVal, B2, CHECK> {
            a: a2,
            b: b2,
            a_val,
        })
            .spec_parse(x)
},