Function lemma_const_spec_parse_congruence 

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

requires

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

ensures

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