Theorem: LO.System.not_inconsistent_iff_consistent (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
⊢ Consistent 𝓢 → ¬Inconsistent 𝓢
Tactic:
rintro ⟨h⟩
State after:
case mk
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
h : ¬Inconsistent 𝓢
⊢ ¬Inconsistent 𝓢

State before:
case mk
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
h : ¬Inconsistent 𝓢
⊢ ¬Inconsistent 𝓢
Tactic:
exact h
State after:
no goals