Function lemma_star_spec_parse_congruence

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

Expand description

requires

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

ensures

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

lemma_star_spec_parse_congruence