simp only [dif_pos x.size.le_refl, dif_neg h]
case h.h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : ¬stop ≤ size x
⊢ (if h : size x ≤ size x then anyM.loop (p a) x (size x) h 0 else anyM.loop (p a) x (size x) (_ : size x ≤ size x) 0) =
    if h : stop ≤ size x then anyM.loop (p a) x stop h 0 else anyM.loop (p a) x (size x) (_ : size x ≤ size x) 0
no goals