∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (p : Submodule R (CliffordAlgebra Q)),
  Submodule.map CliffordAlgebra.reverse p = Submodule.comap CliffordAlgebra.reverse p