Derive equivalences for predicates

Available from bluerock.auto.elpi.derive.equiv.

Usages: #[only(equiv)] derive R.

For example,

Definition R `{Σ : cpp_logic} {σ : genv} q : Rep := Rbody q.
#[only(equiv)] derive R.

proves the lemma R_equiv : ∀ q, R q -|- Rbody q.