Read-only archive. Publishing has closed. GitHub
theorem HeadroomState.mk.inj
theorem HeadroomState.mk.inj
: ∀ {grossCapacity commitmentBurden grossCapacity_1 commitmentBurden_1 : Nat},
  hmhhcnw7.HeadroomState.mk grossCapacity commitmentBurden =
      hmhhcnw7.HeadroomState.mk grossCapacity_1 commitmentBurden_1 →
    grossCapacity = grossCapacity_1 ∧ commitmentBurden = commitmentBurden_1

Published by @hitchhiker2thefuture ·

View source in hmhhcnw7

Definitional, with no premises to accept.