constructor
case cons.h_2.isFalse.isFalse.head
n : Nat
l : 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 (l.fst, !l.snd) = true
h✝ : ¬acc✝.clause.contains l = true
h2 :
  (let clause := l :: acc✝.clause;
    let_fun nodupkey := ⋯;
    let_fun nodup := ⋯;
    some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ l :: acc✝.clause
no goals