rw [← hc]
case h.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : rupHints[↑idx] < f.clauses.size
hc : f.clauses.get ⟨rupHints[↑idx], h✝⟩ = some c
⊢ some c ∈ f.clauses.data
case h.isTrue
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
h✝ : rupHints[↑idx] < f.clauses.size
hc : f.clauses.get ⟨rupHints[↑idx], h✝⟩ = some c
⊢ f.clauses.get ⟨rupHints[↑idx], h✝⟩ ∈ f.clauses.data