have hIF₁ : Irreflexive F₁.Rel' := by exact f;
case intro
α : Type
M₁ M₂ : Model α
F₁✝ : Frame' α
F₂ : Frame' α
f : ?m.28793
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 }
⊢ False
case intro
α : 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'
⊢ False