. rw [← h4]
  apply List.get_mem
case h_3.inl.h.isTrue.intro.isFalse
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : f.clauses[id]! = some val✝
h✝¹ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h✝ : ¬id = ↑i
h4 : f.clauses.data.get ⟨↑i, ⋯⟩ = some c
⊢ some c ∈ f.clauses.data
no goals