theorem LO.IntProp.Hilbert.iff_provable_dn_efq_dne_provable {α : Type u_1} [DecidableEq α] {φ : LO.IntProp.Formula α} : LO.IntProp.Hilbert.Int α ⊢! ∼∼φ ↔ LO.IntProp.Hilbert.Cl α ⊢! φ

theorem LO.IntProp.Hilbert.glivenko {α : Type u_1} [DecidableEq α] {φ : LO.IntProp.Formula α} : LO.IntProp.Hilbert.Int α ⊢! ∼∼φ ↔ LO.IntProp.Hilbert.Cl α ⊢! φ

Alias of LO.IntProp.Hilbert.iff_provable_dn_efq_dne_provable.

theorem LO.IntProp.Hilbert.iff_provable_neg_efq_provable_neg_efq {α : Type u_1} [DecidableEq α] {φ : LO.IntProp.Formula α} : LO.IntProp.Hilbert.Int α ⊢! ∼φ ↔ LO.IntProp.Hilbert.Cl α ⊢! ∼φ