Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case intro.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld : (collection R).fst
star_rel : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
hyp :
  Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inl () ∧
    ∃ y,
      Sum.inr ⟨R, oldWorld⟩ ≠ y ∧
        relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) y ∧
          Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) y (Sum.inl ())
u : Unit ⊕ (k : β) × (collection k).fst
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ u
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) u
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) u (Sum.inl ())
⊢ False
Tactic:
cases u
Proof state after:
case intro.intro.intro.inl
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld : (collection R).fst
star_rel : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
hyp :
  Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inl () ∧
    ∃ y,
      Sum.inr ⟨R, oldWorld⟩ ≠ y ∧
        relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) y ∧
          Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) y (Sum.inl ())
val✝ : Unit
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inl val✝
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inl val✝) (Sum.inl ())
⊢ False

case intro.intro.intro.inr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld : (collection R).fst
star_rel : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
hyp :
  Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inl () ∧
    ∃ y,
      Sum.inr ⟨R, oldWorld⟩ ≠ y ∧
        relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) y ∧
          Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) y (Sum.inl ())
val✝ : (k : β) × (collection k).fst
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inr val✝
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inr val✝)
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr val✝) (Sum.inl ())
⊢ False