case a.h.a
α : Type u_1
β : Type ?u.12137
γ : Type ?u.12140
r : Rel α β
x y : α
⊢ inv Eq x y ↔ x = y
α : Type u_1
β : Type ?u.12137
γ : Type ?u.12140
r : Rel α β
⊢ inv Eq = Eq
ext (x y)
no goals
case a.h.a
α : Type u_1
β : Type ?u.12137
γ : Type ?u.12140
r : Rel α β
x y : α
⊢ inv Eq x y ↔ x = y
constructor <;> apply Eq.symm