intro clause hclause
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray clauses)) → assign ⊨ x
⊢ ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray (none :: clauses))) → assign ⊨ x
n : Nat
clauses : List (Option (DefaultClause n))
h : unsatisfiable (PosFin n) (DefaultFormula.ofArray (List.toArray (none :: clauses)))
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (List.toArray clauses)) → assign ⊨ x
clause : DefaultClause n
hclause : clause ∈ Formula.toList (DefaultFormula.ofArray (List.toArray (none :: clauses)))
⊢ assign ⊨ clause