intro h
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
⊢ insertUnit_invariant assignments0 assignments0_size units assignments assignments_size →
    let update_res := insertUnit (units, assignments, foundContradiction) l;
    let_fun update_res_size := ⋯;
    insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
h : insertUnit_invariant assignments0 assignments0_size units assignments assignments_size
⊢ let update_res := insertUnit (units, assignments, foundContradiction) l;
  let_fun update_res_size := ⋯;
  insertUnit_invariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size