refine Eq.trans (size_shrink_loop as ?_) ?_
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size (shrink as n) = n
case refine_1
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - n ≤ size as

case refine_2
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - (size as - n) = n