∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {inst : CommRing A} {inst_1 : Monoid G}
  {inst_2 : AddCommMonoid V} {inst_3 : AddCommMonoid W} {inst_4 : Module A V} {inst_5 : Module A W}
  {ρ : Representation A G V} {σ : Representation A G W} (motive : ρ.IntertwiningMap σ → Prop) (h : ρ.IntertwiningMap σ),
  (∀ (toFun : V → W) (map_add' : ∀ (x y : V), toFun (x + y) = toFun x + toFun y)
      (map_smul' : ∀ (m : A) (x : V), toFun (m • x) = (RingHom.id A) m • toFun x)
      (isIntertwining' : ∀ (g : G) (v : V), toFun ((ρ g) v) = (σ g) (toFun v)),
      motive { toFun := toFun, map_add' := map_add', map_smul' := map_smul', isIntertwining' := isIntertwining' }) →
    motive h