Function lemma_sum_spec_parse_congruence 

pub proof fn lemma_sum_spec_parse_congruence<A1: SpecParser, A2: SpecParser<PVal = A1::PVal>, B1: SpecParser, B2: SpecParser<PVal = B1::PVal>>(
    a1: A1,
    a2: A2,
    b1: B1,
    b2: B2,
)

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] Sum::<A1, B1>::Inl(a1).spec_parse(x)
        == Sum::<A2, B2>::Inl(a2).spec_parse(x)
},

forall |x: Seq<u8>| {
    #[trigger] Sum::<A1, B1>::Inr(b1).spec_parse(x)
        == Sum::<A2, B2>::Inr(b2).spec_parse(x)
},