COQ Proof Assistant - Примените гипотезу

Question

Я работаю над очень простым заданием доказательства в Coqide.
Я пытаюсь применить гипотезу H2 к моей подцели , но по какой-то причине она не работает , Я не могу понять, почему; Может кто-нибудь объяснить, почему apply H2. команда не применима.

2 subgoals
A : Type
x : A
l1, l2 : list A
H : Prefix l1 l2
H2 : x :: l2 = (x :: l1) ++ [] -> Prefix (x :: l1) (x :: l2)
______________________________________(1/2)
x :: l2 = (x :: l1) ++ []
______________________________________(2/2)
exists l3 : list A, x :: l2 = (x :: l1) ++ l3

Answer 1

apply H2 не имеет возможности работать, потому что его вывод - Prefix (x :: l1) (x :: l2), что не похоже на вашу цель. Посылка H2 - это ваша цель: x :: l2 = (x :: l1) ++ [] однако, это означает, что вы можете apply H2 только если вам удастся сначала решить свою цель ... не очень полезно.