fn parse_axiom(cx: &mut ParseCtxt<'_>) -> ParseResult<Axiom>
⟨axiom⟩ := axiom ⟨ident⟩ ( ⟨refine_param⟩,* ) ⟨block⟩