theorem proved term proof

`prior_holds`

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

formal statement (Lean)

  22theorem prior_holds : ∀ model, mdl_prior model = Cost.Jcost := by

Term-mode proof.

  23  intro model
  24  simp [mdl_prior]
  25
  26end Information
  27end IndisputableMonolith

Lean names referenced from this declaration's body.