Derive_plugin.Deriveval start_deriving : atts:Vernacentries.DefAttributes.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Names.Id.t -> Declare.Proof.tstart_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.