unfold anyPairM.loop
case refl
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
i j : Nat
hij : i < j
h : 0 ≤ 0
⊢ anyPairM.loop #[] p 0 h i j hij = pure false
case refl
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
i j : Nat
hij : i < j
h : 0 ≤ 0
⊢ (if hj : j < 0 then
      let_fun this := (_ : i < size #[]);
      let_fun this_1 := (_ : j < size #[]);
      do
      let __do_lift ← p #[][i] #[][j]
      if __do_lift = true then pure true else anyPairM.loop #[] p 0 h i (j + 1) (_ : i < Nat.succ j)
    else if i < 0 then anyPairM.loop #[] p 0 h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false) =
    pure false