case L => exact ‹a₁ ≃ a₂›
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
left✝ : a₁ ≃ a₂
right✝ : b₁ ≃ b₂
⊢ dffp (a₁, b₁) Hand.L ≃ dffp (a₂, b₂) Hand.L
no goals