Function lemma_parser_congruent_symmetric 

pub proof fn lemma_parser_congruent_symmetric<A, B>(a: A, b: B)
where
    A: SpecParser,
    B: SpecParser<PVal = A::PVal>,

requires

parser_congruent(a, b),

ensures

parser_congruent(b, a),