case H.H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
x✝¹ : β ≃ δ
x✝ : α
⊢ ↑(↑(equivCongr ab cd).symm x✝¹) x✝ = ↑(↑(equivCongr ab.symm cd.symm) x✝¹) x✝
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
⊢ (equivCongr ab cd).symm = equivCongr ab.symm cd.symm
ext
no goals
case H.H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
x✝¹ : β ≃ δ
x✝ : α
⊢ ↑(↑(equivCongr ab cd).symm x✝¹) x✝ = ↑(↑(equivCongr ab.symm cd.symm) x✝¹) x✝
rfl