Function lemma_opt_spec_parse_congruence

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

lemma_opt_spec_parse_congruence