blob: f149b4e8ae749126287fa90fc5bc5fb21e36fa45 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
From Coq Require Import Setoid ssreflect.
Lemma test A (R : relation A) `{Equivalence _ R} (x y z : A) :
R x y -> R y z -> R x z.
Proof.
intros Hxy Hyz.
rewrite -Hxy in Hyz.
exact Hyz.
Qed.
Axiom envs_lookup_delete : bool.
Axiom envs_lookup_delete_Some : envs_lookup_delete = true <-> False.
Goal envs_lookup_delete = true -> False.
Proof.
intros Hlookup.
rewrite envs_lookup_delete_Some in Hlookup *. (* <- used to revert Hlookup *)
exact Hlookup.
Qed.
|
