Function lemma_parser_congruent_intro 

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

requires

forall |input: Seq<u8>| #[trigger] a.spec_parse(input) == b.spec_parse(input),

ensures

#[trigger] parser_congruent(a, b),