blob: ef991365d5e6df8fd705d8461b903967c6559e76 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Import List.
Open Scope list_scope.
Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
let k :=
(match H in (_ = y) return x = hd x y with
| eq_refl => eq_refl
end : x = x')
in k = k.
simpl.
intros.
match goal with
| [ |- appcontext G[@hd] ] => idtac
end.
|
