Невозможно объединить две одинаковые гипотезы

Question

У меня есть две гипотезы в контексте, но когда я пытаюсь apply одна к другой, я получаю ошибку unable to unify. Я должен быть в состоянии объединить их. Две гипотезы следующие: 1003 *

IHl : forallb func l = true -> All (fun x : X => func x = true) l H1 : All (fun x : X => func x = true) l

Моя цель - получить посылку от IHl, применив IHl к H1.

Answer 1

Это распространенная путаница среди начинающих. При использовании гипотезы тактика apply работает следующим образом: если H1 : A -> B и H2 : A, apply H1 in H2 заменяет H2 на H2 : B. Таким образом, чтобы ваше доказательство было успешным, вы должны иметь обратное значение IHl : All ... l -> forallb func l = true в контексте или гипотезу H1 : forallb func l = true.