simp[IsomorphicType.equiv]
α : Type u_2
β : Type ?u.2581
γ : Type ?u.2584
α' : outParam (Type u_1)
β' : outParam (Type ?u.2592)
γ' : outParam (Type ?u.2596)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
a b : α
⊢ (IsomorphicType.equiv tag) a = (IsomorphicType.equiv tag) b → a = b
no goals