intro heq
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ ¬c.clause = [l]
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
heq : c.clause = [l]
⊢ False