no goals
m : Type u_1 → Type u_2
ρ α✝ : Type u_1
p : α✝ → Prop
x : ReaderT ρ m α✝
inst✝ : Monad m
a : ReaderT ρ m { a // p a }
⊢ Subtype.val <$> a = x ↔ ∀ (x_1 : ρ), Subtype.val <$> a x_1 = x x_1
exact ⟨fun eq _ => eq ▸ rfl, funext⟩