exact not_satisfiable_iff_eq_bot.mp (mt h₁ bot_not_satisfiable)
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable ⊥
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
this : ¬satisfiable F
⊢ F = ⊥
no goals