. intro l l_in_nil
  simp only [List.find?, List.not_mem_nil] at l_in_nil
case h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i
no goals