∀ {p : ℕ} {inst : Fact (Nat.Prime p)} {k : Type u_1} {inst_1 : CommRing k} {inst_2 : CharP k p}
  {inst_3 : PerfectRing k p} {V : Type u_2} {inst_4 : AddCommGroup V} {inst_5 : WittVector.Isocrystal p k V}
  {V₂ : Type u_3} {inst_6 : AddCommGroup V₂} {inst_7 : WittVector.Isocrystal p k V₂}
  {toLinearMap : V →ₗ[FractionRing (WittVector p k)] V₂}
  {frob_equivariant :
    ∀ (x : V),
      (WittVector.Isocrystal.frobenius p k) (toLinearMap x) = toLinearMap ((WittVector.Isocrystal.frobenius p k) x)}
  {toLinearMap_1 : V →ₗ[FractionRing (WittVector p k)] V₂}
  {frob_equivariant_1 :
    ∀ (x : V),
      (WittVector.Isocrystal.frobenius p k) (toLinearMap_1 x) =
        toLinearMap_1 ((WittVector.Isocrystal.frobenius p k) x)},
  { toLinearMap := toLinearMap, frob_equivariant := frob_equivariant } =
      { toLinearMap := toLinearMap_1, frob_equivariant := frob_equivariant_1 } →
    toLinearMap = toLinearMap_1