exact h1
case h_1
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
x✝ : Option (DefaultClause n)
heq✝ : f.clauses[id]! = none
h1 : c ∈ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }.toList
⊢ c ∈ f.toList
no goals