Copilot.Theorem.Kind2