∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (motive : SkewMonoidAlgebra k G → SkewMonoidAlgebra k G → Sort u_3)
  (a b : G →₀ k) (h_1 : (a b : G →₀ k) → motive { toFinsupp := a } { toFinsupp := b }),
  (match { toFinsupp := a }, { toFinsupp := b } with
    | { toFinsupp := a }, { toFinsupp := b } => h_1 a b) =
    h_1 a b