Function lemma_exact_len_spec_parse_congruence 

pub proof fn lemma_exact_len_spec_parse_congruence<Inner: SpecParser, Inner2: SpecParser<PVal = Inner::PVal>, Len: AsLen>(
    len: Len,
    inner: Inner,
    inner2: Inner2,
)

requires

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

ensures

forall |x: Seq<u8>| {
    #[trigger] ExactLen(len, inner).spec_parse(x) == ExactLen(len, inner2).spec_parse(x)
},