simp [inconsistent_iff_provable_bot, ←not_inconsistent_iff_consistent]
S : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
inst✝¹ : System F S
inst✝ : DeductiveExplosion S
𝓢 : S
⊢ Consistent 𝓢 ↔ 𝓢 ⊬! ⊥
no goals