exact List.foldlRecOn l insertUnit (units, assignments, foundContradiction) hb hl
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
no goals