Theorem: LO.System.inconsistent_iff_theory_eq_univ (Logic/Logic/System.lean)

State before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
⊢ Inconsistent 𝓢 ↔ theory 𝓢 = Set.univ
Tactic:
simp [inconsistent_def, theory, Set.ext_iff]
State after:
no goals