# Module `Derive_plugin.Derive`

`val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Declare.Proof.t`

`start_deriving f suchthat lemma`

starts a proof of`suchthat`

(which can contain references to`f`

) in the context extended by`f:=?x`

. When the proof ends,`f`

is defined as the value of`?x`

and`lemma`

as the proof.