theorem proved wrapper

`firstPassProgram_deliverables_nodup`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  85theorem firstPassProgram_deliverables_nodup :
  86    firstPassDeliverables.Nodup :=

One-line wrapper that applies firstPassDeliverables_nodup.

  87  firstPassDeliverables_nodup
  88

From the project-wide theorem graph. These declarations reference this one in their body.

empiricalProgramCert in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use

Lean names referenced from this declaration's body.

firstPassDeliverables in IndisputableMonolith.Foundation.OptionAEmpiricalDeliverables decl_use
firstPassDeliverables_nodup in IndisputableMonolith.Foundation.OptionAEmpiricalDeliverables decl_use