by_contra hC
α : Type
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
⊢ ¬∃ Ax, ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
α : Type
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : ?m.28793
p : Formula α
T : Theory α
hC : ∃ Ax, ∀ {F : Frame' α}, Irreflexive F.Rel ↔ F ⊧* Ax
⊢ False