. exact Or.inr l'_in_insertUnit_res
case isTrue
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res : l' ∈ (units, assignments, foundContradiction).fst.data
⊢ l' = l ∨ l' ∈ units.data

case isFalse
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res :
  l' ∈
    (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).fst.data
⊢ l' = l ∨ l' ∈ units.data
case isFalse
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
l' : Literal (PosFin n)
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
l'_in_insertUnit_res :
  l' ∈
    (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).fst.data
⊢ l' = l ∨ l' ∈ units.data