rw [hFC] at h₁
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable (F ⊓ C)
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
⊢ F = ⊥
case intro
ν : Type u_1
F C : PropFun ν
h₁ : satisfiable F → satisfiable ⊥
mpr✝ : satisfiable (F ⊓ C) → satisfiable F
hFC : F ⊓ C = ⊥
⊢ F = ⊥