intro mF mR moW
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
⊢ ∀ (f : Formula) (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) f ↔ evaluate (collection R).snd.2.1 oldWorld f
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨mR, moW⟩) mF ↔ evaluate (collection mR).snd.2.1 moW mF