simp only [← heq, empty, List.length_nil] at i
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
c' : DefaultClause n
heq : empty = c'
hsize : c'.clause.length = arr.size - arr.size
i : Fin c'.clause.length
⊢ let_fun idx_in_bounds := ⋯;
  c'.clause.get i = arr[arr.size + ↑i]
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
c' : DefaultClause n
heq : empty = c'
hsize : c'.clause.length = arr.size - arr.size
i✝ : Fin c'.clause.length
i : Fin 0
⊢ let_fun idx_in_bounds := ⋯;
  c'.clause.get i✝ = arr[arr.size + ↑i✝]