intro h0
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
⊢ insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
    insertUnit_invariant assignments0 assignments0_size
      (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
      (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (rupUnits : Array (Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n)
    (b : Bool),
    insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size →
      let update_res := List.foldl insertUnit (rupUnits, assignments, b) tl;
      let_fun update_res_size := ⋯;
      insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
h0 : insertUnit_invariant assignments0 assignments0_size rupUnits assignments assignments_size
⊢ insertUnit_invariant assignments0 assignments0_size
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).fst
    (List.foldl insertUnit (insertUnit (rupUnits, assignments, b) hd) tl).snd.fst ⋯