exact heq
case cons.h_2.isFalse.isFalse.tail.a.h2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 : some { clause := hd :: acc✝.clause, nodupkey := ⋯, nodup := ⋯ } = some lratClause
a✝ : List.Mem l tl
⊢ List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) { data := tl }.data =
    some acc✝
no goals