Function lemma_ref_fn_parser_congruence 

pub broadcast proof fn lemma_ref_fn_parser_congruence<I, O, Spec, Exec>(
    parser: &FnParser<I, O, Spec, Exec>,
)
where
    I: View<V = Seq<u8>>,
    O: DeepView,
    Spec: SpecParser<PVal = O::V>,
    Exec: Fn(&I) -> PResult<O>,

ensures

#[trigger] parser_congruent(parser, parser.spec_fn@),

Connects an executable parser callback, through the Rust reference adapter, directly to its ghost parser. This packages the otherwise repetitive pointwise spec_parse proof.