Read-only archive. Publishing has closed. GitHub
theorem HypotheticalWorldExample.NazisWonWWIIWorld.mk.injEq
theorem HypotheticalWorldExample.NazisWonWWIIWorld.mk.injEq
: ∀ (toModalWorld : r0nkgtza.ModalWorld)
  (holds_eq : r0nkgtza.ModalWorld.holds toModalWorld = Axiom.getSemantics "world where Nazis won WWII")
  (nazis_won : r0nkgtza.ModalWorld.holds toModalWorld q59pcv3b.HypotheticalWorldExample.NazisWon)
  (pre1939 :
    ∀ (p : Prop),
      Axiom.Actual p →
        Axiom.Actual (q59pcv3b.HypotheticalWorldExample.OccurredBefore1939 p) →
          r0nkgtza.ModalWorld.holds toModalWorld p)
  (toModalWorld_1 : r0nkgtza.ModalWorld)
  (holds_eq_1 : r0nkgtza.ModalWorld.holds toModalWorld_1 = Axiom.getSemantics "world where Nazis won WWII")
  (nazis_won_1 : r0nkgtza.ModalWorld.holds toModalWorld_1 q59pcv3b.HypotheticalWorldExample.NazisWon)
  (pre1939_1 :
    ∀ (p : Prop),
      Axiom.Actual p →
        Axiom.Actual (q59pcv3b.HypotheticalWorldExample.OccurredBefore1939 p) →
          r0nkgtza.ModalWorld.holds toModalWorld_1 p),
  (q59pcv3b.HypotheticalWorldExample.NazisWonWWIIWorld.mk toModalWorld holds_eq nazis_won pre1939 =
      q59pcv3b.HypotheticalWorldExample.NazisWonWWIIWorld.mk toModalWorld_1 holds_eq_1 nazis_won_1 pre1939_1) =
    (toModalWorld = toModalWorld_1)

Published by @sam ·

View source in q59pcv3b

Definitional, with no premises to accept.