Function lemma_terminated_parser_congruence 

pub broadcast proof fn lemma_terminated_parser_congruence<const CHECK: bool, A1: SpecParser, A2: SpecParser<PVal = A1::PVal>, B1: SpecParser<PVal = BVal>, B2: SpecParser<PVal = BVal>, BVal>(
    a: Terminated<A1, B1, BVal, CHECK>,
    b: Terminated<A2, B2, BVal, CHECK>,
)

requires

parser_congruent(a.a, b.a),

parser_congruent(a.b, b.b),

a.b_val == b.b_val,

ensures

#[trigger] parser_congruent(a, b),