α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
h1 : as1 = as2
⊢ Equiv as1 as2
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
⊢ as1 = as2 → Equiv as1 as2
intro h1
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
h1 : as1 = as2
⊢ Equiv as2 as2
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
h1 : as1 = as2
⊢ Equiv as1 as2
rw [h1]
no goals
α : Type u
β : Type v
γ : Type w
a : α
as as1 as2 as3 : List α
inst✝¹ : Inhabited α
inst✝ : Inhabited β
h1 : as1 = as2
⊢ Equiv as2 as2
apply equiv_refl