∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  (W W_1 : WeierstrassCurve K) (e_W : W = W_1) [hW : WeierstrassCurve.IsIntegral R W],
  WeierstrassCurve.integralModel R W = WeierstrassCurve.integralModel R W_1