. existsi z;
  constructor;
  . assumption;
  . simp_all [Satisfies, (fInj 0), (fInj 1)];
case intro.intro.intro.intro.intro.intro.intro.intro.right
α : 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_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))
no goals