exact (Or.inr ∘ Or.inr ∘ Exists.intro c) rfl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
⊢ some (some c) = none ∨ some (some c) = some none ∨ ∃ c_1, some (some c) = some (some c_1)
no goals