rw [LRAT.DefaultClause.insert] at h2
case cons.h_2
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
h1 : l ∈ hd :: tl
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✝
h2 : acc✝.insert hd = some lratClause
⊢ l ∈ lratClause.clause
case cons.h_2
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
h1 : l ∈ hd :: tl
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✝
h2 :
  (if heq1 : acc✝.clause.contains (hd.fst, !hd.snd) = true then none
    else
      if heq2 : acc✝.clause.contains hd = true then some acc✝
      else
        let clause := hd :: acc✝.clause;
        let_fun nodupkey := ⋯;
        let_fun nodup := ⋯;
        some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause