{k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_4} →
        {V₂ : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] →
                      [inst_6 : AddTorsor V₂ P₂] →
                        {motive : (P₁ ≃ᵃ[k] P₂) → Sort u} →
                          (t : P₁ ≃ᵃ[k] P₂) →
                            ((toEquiv : P₁ ≃ P₂) →
                                (linear : V₁ ≃ₗ[k] V₂) →
                                  (map_vadd' : ∀ (p : P₁) (v : V₁), toEquiv (v +ᵥ p) = linear v +ᵥ toEquiv p) →
                                    motive { toEquiv := toEquiv, linear := linear, map_vadd' := map_vadd' }) →
                              motive t