theorem proved decidable or rfl

`jCost_before_arithmetic`

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

formal statement (Lean)

  93theorem jCost_before_arithmetic :
  94    Before Stage.jCost Stage.arithmeticObject := by

Decided by rfl or decide.

  95  decide
  96

Lean names referenced from this declaration's body.