Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case right
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : ℕ
⊢ (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
      R₁ ≠ R₂ →
        ¬relate
            ({
                  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
            (·a) (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
    ∀ (R : β) (oldWorld : (collection R).fst),
      ¬relate
          ({
                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
          (·a) (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
Tactic:
aesop
Proof state after:
no goals