aesop
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
⊢ ∀ (a a_1 : Program),
    (fun π =>
          (∀ (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₂) ∧
            (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
                R₁ ≠ R₂ →
                  ¬relate (combinedModel collection newVal).1 π (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
              ∀ (R : β) (oldWorld : (collection R).fst),
                ¬relate (combinedModel collection newVal).1 π (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ()))
        a →
      (fun π =>
            (∀ (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₂) ∧
              (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
                  R₁ ≠ R₂ →
                    ¬relate (combinedModel collection newVal).1 π (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
                ∀ (R : β) (oldWorld : (collection R).fst),
                  ¬relate (combinedModel collection newVal).1 π (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ()))
          a_1 →
        (fun π =>
            (∀ (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₂) ∧
              (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
                  R₁ ≠ R₂ →
                    ¬relate (combinedModel collection newVal).1 π (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
                ∀ (R : β) (oldWorld : (collection R).fst),
                  ¬relate (combinedModel collection newVal).1 π (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ()))
          (a⋓a_1)
no goals