rw [Array.foldr_eq_foldr_data,Array.toArray_data] at h2
case cons
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
h2 :
  (let fold_fn := fun l acc =>
      match acc with
      | none => none
      | some acc => acc.insert l;
    Array.foldr fold_fn (some LRAT.DefaultClause.empty) (List.toArray (hd :: tl)) (List.toArray (hd :: tl)).size) =
    some lratClause
⊢ l ∈ lratClause.clause
case cons
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
h2 :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) { data := hd :: tl }.data =
    some lratClause
⊢ l ∈ lratClause.clause