existsi x
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))
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_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))