all_goals
  simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq]
  exact Or.inl h
case mpr.inr.inl.h.h_1
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
heq✝ : c1.isUnit = none
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }.clauses.data

case mpr.inr.inl.h.h_2
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, true)
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addPosAssignment }.clauses.data

case mpr.inr.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addNegAssignment }.clauses.data
no goals