exact Subtype.eq ∘ Subtype.eq
case refine_2.f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
x₁ x₂ : { a // ¬(q ∘ Subtype.val) a }
⊢ x₁.val.val = x₂.val.val → x₁ = x₂
no goals