have hsize : (ofArray arr).assignments.size = n := by
  simp only [ofArray, Array.foldl_eq_foldl_data]
  have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
  have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.data) :
    (ofArray_fold_fn acc cOpt).size = n := by rw [ofArray_fold_fn_preserves_assignments_size acc cOpt, ih]
  exact List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl
case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).strong_assignments_invariant
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
⊢ (ofArray arr).strong_assignments_invariant