. simp_all [Satisfies, (fInj 0), (fInj 1)];
case intro.intro.intro.intro.intro.intro.intro.intro.left.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
⊢ (∀ (w' : F.World),
      y ≺ 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 }
        y (atom (f 1))
no goals