blob: bbe9d4bfff97443829167456b7df7e3b7d800268 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
Set Keyed Unification.
Section foo.
Variable f : nat -> nat.
Definition g := f.
Variable lem : g 0 = 0.
Goal f 0 = 0.
Proof.
Fail rewrite lem.
Abort.
Declare Equivalent Keys @g @f.
(** Now f and g are considered equivalent heads for subterm selection *)
Goal f 0 = 0.
Proof.
rewrite lem.
reflexivity.
Qed.
Print Equivalent Keys.
End foo.
|
