simp only [LRAT.Formula.formulaHSat_def, List.all_eq_true, decide_eq_true_eq] at *
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))
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