Function lemma_preceded_parser_congruence 

pub broadcast proof fn lemma_preceded_parser_congruence<const CHECK: bool, A1: SpecParser<PVal = AVal>, A2: SpecParser<PVal = AVal>, B1: SpecParser, B2: SpecParser<PVal = B1::PVal>, AVal>(
    a: Preceded<A1, AVal, B1, CHECK>,
    b: Preceded<A2, AVal, B2, CHECK>,
)

requires

parser_congruent(a.a, b.a),

parser_congruent(a.b, b.b),

a.a_val == b.a_val,

ensures

#[trigger] parser_congruent(a, b),