exact indexed_eqvOp.trans ‹f x ≃ g x› ‹g x ≃ h x›
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
x : α
this✝ : f x ≃ g x
this : g x ≃ h x
⊢ f x ≃ h x
no goals