unfold KripkeModel.Rel at *
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 : (collection R).snd.2.1.Rel a oldWorld₁ oldWorld₂
⊢ (combinedModel collection newVal).1.Rel 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 : (collection R).snd.2.1.2 a oldWorld₁ oldWorld₂
⊢ (combinedModel collection newVal).1.2 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩)