simp [ValidOnModel, not_forall, Axioms.Dot3]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ¬ValidOnModel
      { Frame := F,
        Valuation := fun w a =>
          match finv a with
          | 0 => y ≺ w
          | 1 => z ≺ w }
      (Axioms.Dot3 (atom (f 0)) (atom (f 1)))
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ∃ x,
    (∃ x_1,
        x ≺ x_1 ∧
          (∀ (w' : F.World),
              x_1 ≺ w' →
                Satisfies
                  { Frame := F,
                    Valuation := fun w a =>
                      match finv a with
                      | 0 => y ≺ w
                      | 1 => z ≺ w }
                  w' (atom (f 0))) ∧
            ¬Satisfies
                { Frame := F,
                  Valuation := fun w a =>
                    match finv a with
                    | 0 => y ≺ w
                    | 1 => z ≺ w }
                x_1 (atom (f 1))) ∧
      ∃ x_1,
        x ≺ x_1 ∧
          (∀ (w' : F.World),
              x_1 ≺ w' →
                Satisfies
                  { Frame := F,
                    Valuation := fun w a =>
                      match finv a with
                      | 0 => y ≺ w
                      | 1 => z ≺ w }
                  w' (atom (f 1))) ∧
            ¬Satisfies
                { Frame := F,
                  Valuation := fun w a =>
                    match finv a with
                    | 0 => y ≺ w
                    | 1 => z ≺ w }
                x_1 (atom (f 0))