exact ⟨pure ⟨x,rfl⟩, map_pure Subtype.val _⟩
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
h : ¬n < size x
⊢ SatisfiesM (fun y => size y = size x) (pure x)
no goals