Function lemma_ref_spec_parse_congruence

pub proof fn lemma_ref_spec_parse_congruence<Inner1: SpecParser, Inner2: SpecParser<PVal = Inner1::PVal>>(
    inner1: Inner1,
    inner2: Inner2,
)

Expand description

requires

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

ensures

forall |x: Seq<u8>| #[trigger] Ref(inner1).spec_parse(x) == Ref(inner2).spec_parse(x),

lemma_ref_spec_parse_congruence