exact ⟨hsize, h1, h2⟩
case intro.intro.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
h✝ : acc.2.2.snd = true ∨ acc.2.2.fst = true
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) acc
no goals