Derive `Fwd` hints

Available from bluerock.auto.elpi.derive.fwd.

This command does not yet support usages inside Sections.

Usage: #[only(DIR)] derive Lem. where Lem is an equivalence forall ..., LHS ... -|- RHS ... or an entailment forall ..., LHS ... |-- RHS ... registers an exported Fwd hint based on Lem:

if DIR is fwd or fwd(l2r): replace LHS by RHS (corresponds to [FWD->])
if DIR = fwd(l2r): replace RHS by LHS (corresponds to [FWD<-], ONLY for Lem an equivalence)

For example, with

Lemma lemPQ : P |-- Q.
Proof. (* proof of the hint *) Qed.

#[only(fwd)] derive lemPQ.

is similar to

Definition lemPQ_F (* : Fwd P *) := [FWD] lemPQ.