specialize ih hd_res.1 hd_res.2.1 hd_res.2.2
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
ih :
  ∀ (unitsAcc : Array (Literal (PosFin n))) (assignments : Array Assignment) (b : Bool),
    (List.foldl insertUnit (unitsAcc, assignments, b) tl).snd.fst.size = assignments.size
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
hd_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (unitsAcc, asssignments, b) hd
⊢ (List.foldl insertUnit (insertUnit (unitsAcc, asssignments, b) hd) tl).snd.fst.size = asssignments.size
n : Nat
hd : Literal (PosFin n)
tl : List (Literal (PosFin n))
unitsAcc : Array (Literal (PosFin n))
asssignments : Array Assignment
b : Bool
hd_res : Array (Literal (PosFin n)) × Array Assignment × Bool := insertUnit (unitsAcc, asssignments, b) hd
ih : (List.foldl insertUnit (hd_res.fst, hd_res.snd.fst, hd_res.snd.snd) tl).snd.fst.size = hd_res.snd.fst.size
⊢ (List.foldl insertUnit (insertUnit (unitsAcc, asssignments, b) hd) tl).snd.fst.size = asssignments.size