Function lemma_repeat_till_end_spec_parse_congruence

pub proof fn lemma_repeat_till_end_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] RepeatTillEnd(a).spec_parse(x) == RepeatTillEnd(b).spec_parse(x)
},

lemma_repeat_till_end_spec_parse_congruence