theorem ModalWorld.mk.injEq
theorem ModalWorld.mk.injEq
: ∀ (holds : Prop → Prop) (intro : ∀ (p : Prop), p → holds p) (mp : ∀ (p q : Prop), holds (p → q) → holds p → holds q)
  (consistency : ¬holds False) (elim : ∀ (p : Prop), holds (holds p) = holds p) (holds_1 : Prop → Prop)
  (intro_1 : ∀ (p : Prop), p → holds_1 p) (mp_1 : ∀ (p q : Prop), holds_1 (p → q) → holds_1 p → holds_1 q)
  (consistency_1 : ¬holds_1 False) (elim_1 : ∀ (p : Prop), holds_1 (holds_1 p) = holds_1 p),
  (r0nkgtza.ModalWorld.mk holds intro mp consistency elim =
      r0nkgtza.ModalWorld.mk holds_1 intro_1 mp_1 consistency_1 elim_1) =
    (holds = holds_1)