unfold combinedModel 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.2 a oldWorld₁ oldWorld₂
⊢ (combinedModel collection newVal).1.2 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₂
⊢ ({
            val := fun world =>
              Sum.casesOn (motive := fun t => world = t → ℕ → Prop) world
                (fun val h => PUnit.casesOn (motive := fun t => val = t → ℕ → Prop) val (fun h => newVal) ⋯)
                (fun val h =>
                  Sigma.casesOn (motive := fun t => val = t → ℕ → Prop) val (fun R w h => (collection R).snd.2.1.val w)
                    ⋯)
                ⋯,
            Rel := fun prog worldOne worldTwo =>
              Sum.casesOn (motive := fun t => worldOne = t → Prop) worldOne
                (fun val h =>
                  Sum.casesOn (motive := fun t => worldTwo = t → Prop) worldTwo (fun val h => False)
                    (fun val h => HEq val.snd (collection val.fst).snd.2 ∧ HEq prog (collection val.fst).snd.1) ⋯)
                (fun val h =>
                  Sum.casesOn (motive := fun t => worldTwo = t → Prop) worldTwo (fun val h => False)
                    (fun val_1 h =>
                      Sigma.casesOn (motive := fun t => val = t → Prop) val
                        (fun kOne wOne h =>
                          Sigma.casesOn (motive := fun t => val_1 = t → Prop) val_1
                            (fun kTwo wTwo h =>
                              let_fun help := fun same =>
                                let_fun sameCol := ⋯;
                                (collection kOne).snd.2.1.Rel prog wOne (⋯.mp wTwo);
                              if same : kOne = kTwo then help same else False)
                            ⋯)
                        ⋯)
                    ⋯)
                ⋯ },
          Sum.inl ()).1.2
    a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩)