simp_all
case mpr.right.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
R : β
oldWorld : (collection R).fst
otherR : β
otherWorld : (collection otherR).fst
true_in_old :
  ∀ (v : (collection R).fst), relate (collection R).snd.2.1 α oldWorld v → evaluate (collection R).snd.2.1 v f
rel_in_new_model : relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inr ⟨otherR, otherWorld⟩)
IH_f :
  evaluate (combinedModel collection newVal).1 (Sum.inr ⟨otherR, otherWorld⟩) f ↔
    evaluate (collection otherR).snd.2.1 otherWorld f
IH_rel :
  ∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
    relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
      relate (collection R).snd.2.1 α oldWorld₁ oldWorld₂
noNewL :
  ∀ (R : β) (oldWorld : (collection R).fst),
    ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
sameR :
  ¬R = otherR → ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inr ⟨otherR, otherWorld⟩)
⊢ evaluate (collection otherR).snd.2.1 otherWorld f
case mpr.right.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
R : β
oldWorld : (collection R).fst
otherR : β
otherWorld : (collection otherR).fst
true_in_old :
  ∀ (v : (collection R).fst), relate (collection R).snd.2.1 α oldWorld v → evaluate (collection R).snd.2.1 v f
rel_in_new_model : relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inr ⟨otherR, otherWorld⟩)
IH_f :
  evaluate (combinedModel collection newVal).1 (Sum.inr ⟨otherR, otherWorld⟩) f ↔
    evaluate (collection otherR).snd.2.1 otherWorld f
IH_rel :
  ∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
    relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
      relate (collection R).snd.2.1 α oldWorld₁ oldWorld₂
noNewL :
  ∀ (R : β) (oldWorld : (collection R).fst),
    ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
sameR : R = otherR
⊢ evaluate (collection otherR).snd.2.1 otherWorld f