aesop
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
⊢ ∀ (a : ℕ),
    (fun φ =>
        ∀ (R : β) (oldWorld : (collection R).fst),
          evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) φ ↔
            evaluate (collection R).snd.2.1 oldWorld φ)
      (·a)
no goals