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