diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-09-21 20:45:01 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-09-22 10:44:07 -0400 |
| commit | 5357fe92e65712a3e2506fe0a939b358d14183d7 (patch) | |
| tree | ea0328c53e10620d9a46cd13606a5b6646ce7d6f /src/Util/Relations.v | |
| parent | fd5cba50d8743149e7ca4e386716126f2fc03e63 (diff) | |
alternative signing derivation
cleanup
Diffstat (limited to 'src/Util/Relations.v')
| -rw-r--r-- | src/Util/Relations.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Util/Relations.v b/src/Util/Relations.v index aa280db26..4612fa8a8 100644 --- a/src/Util/Relations.v +++ b/src/Util/Relations.v @@ -27,3 +27,8 @@ Proof. logic; try match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end. repeat (assumption||reflexivity||econstructor); assumption. (* WHY the last [assumption]?*) Qed. + +Lemma iff_R_R_same_r {T R} {Req:@Equivalence T R} x y ref : R x y -> (R x ref <-> R y ref). +Proof. + intro Hx; rewrite Hx; clear Hx. reflexivity. +Qed.
\ No newline at end of file |