cases heq
case refine_2.refl.inl
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
heq : j = List.length bs.data
⊢ (push bs (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[j] =
    f as[j] (_ : p as[j])
case refine_2.refl.inl.refl
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
bs : Array β
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
hj : List.length bs.data < List.length bs.data + 1
⊢ (push bs
        (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[List.length bs.data] =
    f as[List.length bs.data] (_ : p as[List.length bs.data])