simp
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
this :
  ∀ (i : Nat),
    i ≤ n →
      ∀ (o : Array α),
        size o = n - i →
          Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
              (Nat.succ i) (n - i) ⋯ o =
            push
              (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i (n - i)
                ⋯ o)
              (f { val := n, isLt := ⋯ })
⊢ size #[] = n - n
no goals