∀ {ι : Type u_1} (S : ι → Type u_2) (x : ((i : ι) → S i)ᵐᵒᵖ),
  (MulOpposite.op fun i => MulOpposite.unop (MulOpposite.op (MulOpposite.unop x i))) =
    MulOpposite.op fun i => MulOpposite.unop (MulOpposite.op (MulOpposite.unop x i))