Function lemma_refined_parser_congruence 

pub broadcast proof fn lemma_refined_parser_congruence<Inner1: SpecParser, Inner2: SpecParser<PVal = Inner1::PVal>, P1: SpecPred<Inner1::PVal>, P2: SpecPred<Inner1::PVal>>(
    a: Refined<Inner1, P1>,
    b: Refined<Inner2, P2>,
)

requires

parser_congruent(a.0, b.0),

forall |v: Inner1::PVal| #[trigger] a.1.apply(v) <==> b.1.apply(v),

ensures

#[trigger] parser_congruent(a, b),