Module Discharge
val process_inductive : Lib.abstr_info -> Opaqueproof.work_list -> Declarations.mutual_inductive_body -> Entries.mutual_inductive_entry
Dischargeval process_inductive : Lib.abstr_info -> Opaqueproof.work_list -> Declarations.mutual_inductive_body -> Entries.mutual_inductive_entry