Я закончил писать довольно длинное доказательство, но всякий раз, когда я пытаюсь Qed, я получаю сообщение об ошибке Error: This proof is focused, but cannot be unfocused this way. Есть ли другие способы расфокусировать Proof? Shoudl, я просто использую признал, хотя мое доказательство является строгим? Для справки я использую CoqIDE 8.6