KV
Size: a a a
2018 April 06
Oℕ
Эта ваша эдукера очень странно себя ведёт
это ты сам ткнул на False elimination
KV
Да, но почему оно чекнулось?
KV
Я вообще не понял, что произошло
Oℕ
Да, но почему оно чекнулось?
А что там справа, что осталось доказать?
KV
Больше ничего
Oℕ
В смысле - всё? Галка на этом?
KV
Oℕ
Ну чо, вот такой вот твой coq unsound,
KV
я вообще на indirect proof нажал
Oℕ
Ну баг. Начни заново
KV
Начал заново, всё воспроизводится
KV
Упражнение 11 в кванторах
Oℕ
аххаха, риальни
AG
да, прикольный баг, с квантором не играет
Oℕ
ну ты проигнорируй и реши нормальр
KV
ну ты проигнорируй и реши нормальр
Ну через indirect proof - это пока единственное, что мне пришло в голову
AG
по моему прямо оно вообще конструктивно решается
AG
там в обратную сторону лем
Oℕ
у меня там Lem вверхц