rw [l'_eq_l'']
case inl
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
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_eq_l'' : l' = l''
⊢ l' ∈ l ∨ l' ∈ units.data
case inl
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
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.data → l' ∈ l ∨ l' ∈ units.data
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.data
l'_eq_l'' : l' = l''
⊢ l'' ∈ l ∨ l'' ∈ units.data