apply h assign
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray (List.toArray clauses)
⊢ False
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray (List.toArray clauses)
⊢ assign ⊨ DefaultFormula.ofArray (List.toArray (none :: clauses))