`BookProof.SmOneParticle.smG_ne_smDG` (a : Fin 8) (i : Fin 3) (b : Fin 8) (k l : Fin 3) : smG a i ≠ smDG b k l

Initializing...

`BookProof.SmOneParticle.smG_ne_smDG` (a : Fin 8) (i : Fin 3) (b : Fin 8) (k l : Fin 3) : smG a i ≠ smDG b k l · Prove2Me