Как доказать, что "(∀x. P) ∧ Q ⟹ ∀x. P", используя конъюнкт1 в Изабель?

Question

Я пытаюсь доказать это:

lemma
  assumes 0: "(∀x. P) ∧ Q"
  shows "∀x. P"
proof -
  show ?thesis using 0 by (rule conjunct1)
qed

Я собираюсь:

Failed to apply initial proof method⌂:
using this:
  (∀x. P) ∧ Q
goal (1 subgoal):
 1. ∀x. P

Что я должен изменить в своем доказательстве?

Answer 1

Вывод типа встал на вашем пути. Если вы исправите тип x в обоих случаях, т.е.

lemma
  assumes 0: "(∀(x::nat). P) ∧ Q"
  shows "∀(x::nat). P"
proof -
  show ?thesis using 0 by (rule conjunct1)
qed

оно работает.

Без аннотации этого типа Изабель делает первый вывод x быть типом 'aпеременная типа, а вторая x получает переменную другого типа.