Как использовать применить для «извлечения» импликации в Coq

Question

Я проиллюстрирую пример.

H : R -> P -> Q 

H0 : R 

подцель:

(Q -> P) \/(P -> Q) 

поэтому мой вопрос, как извлечь из (P-> Q). У меня есть R уже, но когда я «применить Н в Н0», она оценивает все, и дает мне Q.

Answer 1

Вы можете сделать любой из:

specialize (H H0). 

заменить H с H: P -> Q, или:

pose proof (H H0) as H1 

ввести H1: P -> Q

Вы также можете идти вперед:

right. exact (H H0).