have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
  (h : ∀ l' : Literal (PosFin n), l' ∈ acc.1.data → l' ∈ l ∨ l' ∈ units.data) (l'' : Literal (PosFin n))
  (l''_in_l : l'' ∈ l) : ∀ l' : Literal (PosFin n), l' ∈ (insertUnit acc l'').1.data → l' ∈ l ∨ l' ∈ units.data := by
  intro l' l'_in_res
  rcases mem_insertUnit_units  acc.1 acc.2.1 acc.2.2 l'' l' l'_in_res with l'_eq_l'' | l'_in_acc
  . rw [l'_eq_l'']
    exact Or.inl l''_in_l
  . exact h l' l'_in_acc
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.data → l' ∈ l ∨ l' ∈ units.data
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : List (Literal (PosFin n))
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.data → l' ∈ l ∨ l' ∈ units.data
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data) →
      ∀ (l'' : Literal (PosFin n)),
        l'' ∈ l → ∀ (l' : Literal (PosFin n)), l' ∈ (insertUnit acc l'').fst.data → l' ∈ l ∨ l' ∈ units.data
⊢ let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l;
  ∀ (l' : Literal (PosFin n)), l' ∈ insertUnit_fold_res.fst.data → l' ∈ l ∨ l' ∈ units.data