show ∀ (x : α), f x ≃ f x
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f : (x : α) → β x
⊢ f ≃ f
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f : (x : α) → β x
⊢ ∀ (x : α), f x ≃ f x