Function lemma_repeat_spec_parse_congruence 

pub proof fn lemma_repeat_spec_parse_congruence<A: SpecParser, B: SpecParser<PVal = A::PVal>, T: SpecParser>(
    a: A,
    b: B,
    t: T,
)

requires

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

ensures

forall |x: Seq<u8>| #[trigger] Repeat(a, t).spec_parse(x) == Repeat(b, t).spec_parse(x),