case a.h.a
α : Type u_1
β : Type u_2
γ : Type ?u.884
r : Rel α β
x : α
y : β
⊢ inv (inv r) x y ↔ r x y
α : Type u_1
β : Type u_2
γ : Type ?u.884
r : Rel α β
⊢ inv (inv r) = r
ext (x y)
no goals
case a.h.a
α : Type u_1
β : Type u_2
γ : Type ?u.884
r : Rel α β
x : α
y : β
⊢ inv (inv r) x y ↔ r x y
rfl