cases h2
case cons.h_1
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)
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    none
h2 : none = some lratClause
⊢ l ∈ lratClause.clause
no goals