existsi f 0, f 1, (λ w a =>
  match (finv a) with
  | 0 => y ≺ w
  | 1 => z ≺ w
)
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
⊢ ∃ a b x, ¬ValidOnModel { Frame := F, Valuation := x } (Axioms.Dot3 a b)
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)))