Я нахожусь в процессе доказательства леммы в Coq.
Одна из моих гипотез: H0: ~p -> False для некоторого предложения p.
Единственная подцель, которую я оставил, - p
Можно предположить, что есть тактика c, которая позволяет мне доказать p, используя H0 за один шаг. Однако я не могу найти его.
Существует ли такая тактика c, и если да, то какая это?