diff options
| -rw-r--r-- | src/hls/Abstr.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 9bed783..957e265 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -736,6 +736,8 @@ Section CORRECT. Qed.*) Abort. +End CORRECT. + Lemma get_empty: forall r, empty#r = Psingle (Ebase r). Proof. |