Function parser_congruent 

pub open spec fn parser_congruent<A, B>(a: A, b: B) -> bool
where
    A: SpecParser,
    B: SpecParser<PVal = A::PVal>,

{ forall |input: Seq<u8>| a.spec_parse(input) == b.spec_parse(input) }

Pointwise equality of parser denotations. The format types may differ, but their parsed value types must agree.