exact h
case assignments.intro.h₂.inl.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
motive : Nat → Array Assignment → Prop := f.clear_insert_induction_motive ⋯ (f.insertRupUnits units).fst.rupUnits
h_base : motive 0 (f.insertRupUnits units).fst.assignments
h_inductive :
  ∀ (idx : Fin (f.insertRupUnits units).fst.rupUnits.size) (assignments : Array Assignment),
    motive (↑idx) assignments → motive (↑idx + 1) (clearUnit assignments (f.insertRupUnits units).fst.rupUnits[idx])
h_size :
  (Array.foldl (fun b => clearUnit b) (f.insertRupUnits units).fst.assignments (f.insertRupUnits units).fst.rupUnits
        0).size =
    n
i : Nat
hi1 : i < (Array.foldl clearUnit (f.insertRupUnits units).1.assignments (f.insertRupUnits units).1.rupUnits 0).size
hi2 : i < f.assignments.size
i_lt_n : i < n
h :
  (Array.foldl (fun b => clearUnit b) (f.insertRupUnits units).fst.assignments (f.insertRupUnits units).fst.rupUnits
        0)[↑⟨i, i_lt_n⟩] =
    f.assignments[↑⟨i, i_lt_n⟩]
right✝ :
  ∀ (j : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ↑j ≥ (f.insertRupUnits units).fst.rupUnits.size → (f.insertRupUnits units).fst.rupUnits[j].fst.val ≠ ↑⟨i, i_lt_n⟩
⊢ (Array.foldl clearUnit (f.insertRupUnits units).1.assignments (f.insertRupUnits units).1.rupUnits 0)[i] =
    f.assignments[i]
no goals