intro R oldWorld₁ oldWorld₂
case left
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : ℕ
⊢ ∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
    relate (combinedModel collection newVal).1 (·a) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
      relate (collection R).snd.2.1 (·a) oldWorld₁ oldWorld₂
case left
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : ℕ
R : β
oldWorld₁ oldWorld₂ : (collection R).fst
⊢ relate (combinedModel collection newVal).1 (·a) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
    relate (collection R).snd.2.1 (·a) oldWorld₁ oldWorld₂