Function lemma_parser_congruent_transitive 

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

requires

parser_congruent(a, b),

parser_congruent(b, c),

ensures

parser_congruent(a, c),