rcases c'_in_f with ⟨i, c'_in_f⟩
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
c'_in_f : ∃ n_1, f.clauses.data.get n_1 = some c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses.data.get i = some c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'