Function lemma_star_parse_rec_congruence 

pub proof fn lemma_star_parse_rec_congruence<A: SpecParser, B: SpecParser<PVal = A::PVal>>(
    a: A,
    b: B,
    ibuf: Seq<u8>,
)

requires

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

ensures

Star(a).parse_rec(ibuf) == Star(b).parse_rec(ibuf),