Module Lemmas.Recthm

type t = {
name : Names.Id.t;

Name of theorem

typ : EConstr.t;

Type of theorem

args : Names.Name.t list;

Names to pre-introduce

impargs : Impargs.manual_implicits;

Explicitily declared implicit arguments

}