Document rare_rewrite
In the same spirit of documenting the BV rules, cvc5's Alethe output also produces RARE proof steps. The format we have converged for that is:
(step <id> <conclusion> :rule rare_rewrite :args (<rareRule> (<term>)*)
where is a string value supposed to stand for the name of the rule and may contain an operator "rare-list" whose arity is >= 0 (this operator is to model that arguments of rare rules can be lists of terms).
Somewhere there is a documentation RARE that should be linked. @Lachnitt will know more.