Я создал среду, чтобы попытаться доказать, что мне нужно / нужно
У меня есть функция posfijo, которая сообщает, содержит ли список (l1) другой список (l2) в конце.
Поэтому, если я добавлю элемент в первый список и использую результат в качестве второго списка, например l2 = x :: l1, я хочу доказать, что это невозможно.
Я сделал это ...
Variable G:Set.
Inductive posfijo : list _ -> list _ -> Prop :=
| posfijoB : forall l: list _, posfijo l l
| posfijoI : forall (l1 l2: list _) (a : G), posfijo l1 l2 -> posfijo l1 (cons a l2).
Infix "<<" := (posfijo) (at level 70, right associativity).
Lemma Pref4_a : forall (X:Set)(l: list G)(x:G), ~ (cons x l << l).
Proof.
intros X l x H.
Итак, моя цель:
