1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
Definition var := nat.
Module Import A.
Class Rename (term : Type) := rename : (var -> var) -> term -> term.
End A.
Inductive tm : Type :=
(* | tv : vl_ -> tm *)
with vl_ : Type :=
| var_vl : var -> vl_.
Definition vl := vl_.
Fixpoint tm_rename (sb : var -> var) (t : tm) : tm :=
let b := vl_rename : Rename vl in
match t with
end
with
vl_rename (sb : var -> var) v : vl :=
let a := tm_rename : Rename tm in
let b := vl_rename : Rename vl in
match v with
| var_vl x => var_vl (sb x)
end.
#[export] Instance rename_vl : Rename vl := vl_rename.
Lemma foo ξ x: rename_vl ξ (var_vl x) = var_vl x.
(* Succeeds *)
cbn. Abort.
Lemma foo ξ x: rename ξ (var_vl x) = var_vl x.
(* Fails *)
cbn.
Abort.
|
