Function lemma_bind_parser_congruence 

pub broadcast proof fn lemma_bind_parser_congruence<A1: SpecParser, A2: SpecParser<PVal = A1::PVal>, B1: SpecMap<Input = A1::PVal>, B2: SpecMap<Input = A2::PVal>>(
    a: Bind<A1, B1>,
    b: Bind<A2, B2>,
)
where
    B1::Output: SpecParser,
    B2::Output: SpecParser<PVal = <B1::Output as SpecParser>::PVal>,

requires

parser_congruent(a.0, b.0),

forall |key: A1::PVal| #[trigger] parser_congruent(a.1.spec_map(key), b.1.spec_map(key)),

ensures

#[trigger] parser_congruent(a, b),