val import : ?loc:L.t -> string -> tval data : ?loc:L.t -> ?attrs:T.t list -> t list -> tval defs : ?loc:L.t -> ?attrs:T.t list -> t list -> tval rewrite : ?loc:L.t -> ?attrs:T.t list -> T.t -> tval goal : ?loc:L.t -> ?attrs:T.t list -> T.t -> tval assume : ?loc:L.t -> ?attrs:T.t list -> T.t -> tval lemma : ?loc:L.t -> ?attrs:T.t list -> T.t -> t