Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 α oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_f :
  ∀ (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) f ↔ evaluate (collection R).snd.2.1 oldWorld f
R : β
oldWorld : (collection R).fst
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) (⌈α⌉f) ↔
    evaluate (collection R).snd.2.1 oldWorld (⌈α⌉f)
Tactic:
constructor
Proof state after:
case mp
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 α oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_f :
  ∀ (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) f ↔ evaluate (collection R).snd.2.1 oldWorld f
R : β
oldWorld : (collection R).fst
⊢ evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) (⌈α⌉f) →
    evaluate (collection R).snd.2.1 oldWorld (⌈α⌉f)

case mpr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
α : Program
f : Formula
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 α oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 α (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
IH_f :
  ∀ (R : β) (oldWorld : (collection R).fst),
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) f ↔ evaluate (collection R).snd.2.1 oldWorld f
R : β
oldWorld : (collection R).fst
⊢ evaluate (collection R).snd.2.1 oldWorld (⌈α⌉f) →
    evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) (⌈α⌉f)