next hne =>
simp only [false_iff]
intro heq
exact hne l heq
case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : List (Literal (PosFin n))
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]
no goals