intro h assign hassign
n : Nat
clauses : List (Option (DefaultClause n))
⊢ unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses))) →
    unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray clauses))
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