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