no goals
α✝ : Sort ?u.7280
β✝ : Sort ?u.7283
γ : Sort ?u.7286
p✝ q : α✝ → Prop
α : Sort u_1
β : Sort u_2
f : α → β
p : β → Prop
h : ∀ (a : α), p (f a)
hf : Injective f
x y : α
hxy : coind f h x = coind f h y
⊢ f x = f y
apply congr_arg Subtype.val hxy