intro
case left.h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
⊢ Sum.inl a ≺ Sum.inr ()
case left.h
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂✝ : Frame' α
f✝ : Irreflexive Frame.Rel'
p : Formula α
T : Theory α
Ax : AxiomSet α
h : ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
F₁ : Frame' α := { World := Unit ⊕ Unit, World_nonempty := ⋯, Rel := fun w v => w ≠ v }
hIF₁ : Irreflexive Frame.Rel'
F₂ : Frame' α := { World := Unit, World_nonempty := ⋯, Rel := fun w v => w = v }
hIF₂ : ¬Irreflexive Frame.Rel'
f : F₁.World → F₂.World := fun x => ()
hSur : Function.Surjective f
a : Unit
a✝ : Sum.inl a = Sum.inr ()
⊢ False