1
Set Implicit Arguments.
3
Record Place (Env A: Type) : Type := {
5
write: Env -> A -> Env ;
6
write_read: forall (e:Env), (write e (read e))=e
9
Hint Rewrite -> write_read: placeeq.
11
Record sumPl (Env A B: Type) (vL:(Place Env A)) (vR:(Place Env B)) : Type :=
13
mkEnv: A -> B -> Env ;
14
mkEnv2writeL: forall (e:Env) (x:A), (mkEnv x (read vR e))=(write vL e x)
17
(* when the following line is commented, the bug does not appear *)
18
Hint Rewrite -> mkEnv2writeL: placeeq.
20
Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
21
(exists e1:Env, e=(write p e1 (read p e))).
23
intros Env A e p; eapply ex_intro.
24
autorewrite with placeeq. (* Here is the bug *)