LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock0

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block0 (i : Var) (p q : Fin 3) : SiIntGoal ⟨0, ⋯⟩ i p q