diff --git a/_CoqProject b/_CoqProject
index d8213fe7d866dc030d6f350bdd74b65fdb3d26e1..094baa0edbe3ba252343993b7fadc8b1e41f05ae 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -69,5 +69,6 @@ program_logic/ghost_ownership.v
 heap_lang/heap_lang.v
 heap_lang/heap_lang_tactics.v
 heap_lang/lifting.v
-heap_lang/sugar.v
+heap_lang/derived.v
+heap_lang/notation.v
 heap_lang/tests.v
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
new file mode 100644
index 0000000000000000000000000000000000000000..e8b52a276203cbf8b524616611a1b762137d2a27
--- /dev/null
+++ b/heap_lang/derived.v
@@ -0,0 +1,62 @@
+Require Export heap_lang.lifting.
+Import uPred.
+
+(** Define some derived forms, and derived lemmas about them. *)
+Notation Lam x e := (Rec "" x e).
+Notation Let x e1 e2 := (App (Lam x e2) e1).
+Notation Seq e1 e2 := (Let "" e1 e2).
+Notation LamV x e := (RecV "" x e).
+Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
+Notation SeqCtx e2 := (LetCtx "" e2).
+
+Section derived.
+Context {Σ : iFunctor}.
+Implicit Types P : iProp heap_lang Σ.
+Implicit Types Q : val → iProp heap_lang Σ.
+
+(** Proof rules for the sugar *)
+Lemma wp_lam E x ef e v Q :
+  to_val e = Some v → ▷ wp E (gsubst ef x e) Q ⊑ wp E (App (Lam x ef) e) Q.
+Proof.
+  intros <-%of_to_val; rewrite -wp_rec ?to_of_val //.
+  by rewrite (gsubst_correct _ _ (RecV _ _ _)) subst_empty.
+Qed.
+
+Lemma wp_let E x e1 e2 v Q :
+  to_val e1 = Some v → ▷ wp E (gsubst e2 x e1) Q ⊑ wp E (Let x e1 e2) Q.
+Proof. apply wp_lam. Qed.
+
+Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, ▷ wp E e2 Q) ⊑ wp E (Seq e1 e2) Q.
+Proof.
+  rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
+  by rewrite -wp_let //= ?gsubst_correct ?subst_empty ?to_of_val.
+Qed.
+
+Lemma wp_le E (n1 n2 : nat) P Q :
+  (n1 ≤ n2 → P ⊑ ▷ Q (LitV $ LitBool true)) →
+  (n2 < n1 → P ⊑ ▷ Q (LitV $ LitBool false)) →
+  P ⊑ wp E (BinOp LeOp (Lit $ LitNat n1) (Lit $ LitNat n2)) Q.
+Proof.
+  intros. rewrite -wp_bin_op //; [].
+  destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
+Qed.
+
+Lemma wp_lt E (n1 n2 : nat) P Q :
+  (n1 < n2 → P ⊑ ▷ Q (LitV $ LitBool true)) →
+  (n2 ≤ n1 → P ⊑ ▷ Q (LitV $ LitBool false)) →
+  P ⊑ wp E (BinOp LtOp (Lit $ LitNat n1) (Lit $ LitNat n2)) Q.
+Proof.
+  intros. rewrite -wp_bin_op //; [].
+  destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
+Qed.
+
+Lemma wp_eq E (n1 n2 : nat) P Q :
+  (n1 = n2 → P ⊑ ▷ Q (LitV $ LitBool true)) →
+  (n1 ≠ n2 → P ⊑ ▷ Q (LitV $ LitBool false)) →
+  P ⊑ wp E (BinOp EqOp (Lit $ LitNat n1) (Lit $ LitNat n2)) Q.
+Proof.
+  intros. rewrite -wp_bin_op //; [].
+  destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
+Qed.
+
+End derived.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index d80bf59c0aa64d613d6f8755a4c5541f3ab4f070..8c078f9b9c2b31f719208b29ceb2f3a74e2cfc6d 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,6 +1,7 @@
 Require Import prelude.gmap program_logic.lifting program_logic.ownership.
 Require Export program_logic.weakestpre heap_lang.heap_lang_tactics.
-Import uPred heap_lang.
+Export heap_lang. (* Prefer heap_lang names over language names. *)
+Import uPred.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
 
 (** The substitution operation [gsubst e x ev] behaves just as [subst] but
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
new file mode 100644
index 0000000000000000000000000000000000000000..f7ff70f72df31b99e71fe6340c3a63403882ab14
--- /dev/null
+++ b/heap_lang/notation.v
@@ -0,0 +1,44 @@
+Require Export heap_lang.derived.
+
+Delimit Scope lang_scope with L.
+Bind Scope lang_scope with expr val.
+Arguments wp {_ _} _ _%L _.
+
+Coercion LitNat : nat >-> base_lit.
+Coercion LitBool : bool >-> base_lit.
+(** No coercion from base_lit to expr. This makes is slightly easier to tell
+   apart language and Coq expressions. *)
+Coercion Var : string >-> expr.
+Coercion App : expr >-> Funclass.
+Coercion of_val : val >-> expr.
+
+(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
+    first. *)
+(* What about Arguments for hoare triples?. *)
+Notation "' l" := (LitV l) (at level 8, format "' l") : lang_scope.
+Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope.
+Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope.
+Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
+  (at level 50, left associativity) : lang_scope.
+Notation "e1 - e2" := (BinOp MinusOp e1%L e2%L)
+  (at level 50, left associativity) : lang_scope.
+Notation "e1 ≤ e2" := (BinOp LeOp e1%L e2%L) (at level 70) : lang_scope.
+Notation "e1 < e2" := (BinOp LtOp e1%L e2%L) (at level 70) : lang_scope.
+Notation "e1 = e2" := (BinOp EqOp e1%L e2%L) (at level 70) : lang_scope.
+(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
+Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope.
+Notation "'rec:' f x := e" := (Rec f x e%L)
+  (at level 102, f at level 1, x at level 1, e at level 200) : lang_scope.
+Notation "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
+  (at level 200, e1, e2, e3 at level 200) : lang_scope.
+
+(** Derived notions, in order of declaration. The notations for let and seq
+are stated explicitly instead of relying on the Notations Let and Seq as
+defined above. This is needed because App is now a coercion, and these
+notations are otherwise not pretty printed back accordingly. *)
+Notation "λ: x , e" := (Lam x e%L)
+  (at level 102, x at level 1, e at level 200) : lang_scope.
+Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L)
+  (at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
+Notation "e1 ; e2" := (Lam "" e2%L e1%L)
+  (at level 100, e2 at level 200) : lang_scope.
diff --git a/heap_lang/sugar.v b/heap_lang/sugar.v
deleted file mode 100644
index 98c53efb08e04f302e5ccdecb648dc6ad90e3ea4..0000000000000000000000000000000000000000
--- a/heap_lang/sugar.v
+++ /dev/null
@@ -1,108 +0,0 @@
-Require Export heap_lang.heap_lang heap_lang.lifting.
-Import uPred heap_lang.
-
-(** Define some syntactic sugar. *)
-Notation Lam x e := (Rec "" x e).
-Notation Let x e1 e2 := (App (Lam x e2) e1).
-Notation Seq e1 e2 := (Let "" e1 e2).
-Notation LamV x e := (RecV "" x e).
-Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
-Notation SeqCtx e2 := (LetCtx "" e2).
-
-Module notations.
-  Delimit Scope lang_scope with L.
-  Bind Scope lang_scope with expr val.
-  Arguments wp {_ _} _ _%L _.
-
-  Coercion LitNat : nat >-> base_lit.
-  Coercion LitBool : bool >-> base_lit.
-  (** No coercion from base_lit to expr. This makes is slightly easier to tell
-     apart language and Coq expressions. *)
-  Coercion Var : string >-> expr.
-  Coercion App : expr >-> Funclass.
-  Coercion of_val : val >-> expr.
-
-  (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
-  first. *)
-  (* What about Arguments for hoare triples?. *)
-  Notation "' l" := (LitV l) (at level 8, format "' l") : lang_scope.
-  Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope.
-  Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope.
-  Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
-    (at level 50, left associativity) : lang_scope.
-  Notation "e1 - e2" := (BinOp MinusOp e1%L e2%L)
-    (at level 50, left associativity) : lang_scope.
-  Notation "e1 ≤ e2" := (BinOp LeOp e1%L e2%L) (at level 70) : lang_scope.
-  Notation "e1 < e2" := (BinOp LtOp e1%L e2%L) (at level 70) : lang_scope.
-  Notation "e1 = e2" := (BinOp EqOp e1%L e2%L) (at level 70) : lang_scope.
-  (* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
-  Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope.
-  Notation "'rec:' f x := e" := (Rec f x e%L)
-    (at level 102, f at level 1, x at level 1, e at level 200) : lang_scope.
-  Notation "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
-    (at level 200, e1, e2, e3 at level 200) : lang_scope.
-
-  (** Derived notions, in order of declaration. The notations for let and seq
-  are stated explicitly instead of relying on the Notations Let and Seq as
-  defined above. This is needed because App is now a coercion, and these
-  notations are otherwise not pretty printed back accordingly. *)
-  Notation "λ: x , e" := (Lam x e%L)
-    (at level 102, x at level 1, e at level 200) : lang_scope.
-  Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L)
-    (at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
-  Notation "e1 ; e2" := (Lam "" e2%L e1%L)
-    (at level 100, e2 at level 200) : lang_scope.
-End notations.
-Export notations.
-
-Section sugar.
-Context {Σ : iFunctor}.
-Implicit Types P : iProp heap_lang Σ.
-Implicit Types Q : val → iProp heap_lang Σ.
-
-(** Proof rules for the sugar *)
-Lemma wp_lam E x ef e v Q :
-  to_val e = Some v → ▷ wp E (gsubst ef x e) Q ⊑ wp E (App (Lam x ef) e) Q.
-Proof.
-  intros <-%of_to_val; rewrite -wp_rec ?to_of_val //.
-  by rewrite (gsubst_correct _ _ (RecV _ _ _)) subst_empty.
-Qed.
-
-Lemma wp_let E x e1 e2 v Q :
-  to_val e1 = Some v → ▷ wp E (gsubst e2 x e1) Q ⊑ wp E (Let x e1 e2) Q.
-Proof. apply wp_lam. Qed.
-
-Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, ▷ wp E e2 Q) ⊑ wp E (Seq e1 e2) Q.
-Proof.
-  rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
-  by rewrite -wp_let //= ?gsubst_correct ?subst_empty ?to_of_val.
-Qed.
-
-Lemma wp_le E (n1 n2 : nat) P Q :
-  (n1 ≤ n2 → P ⊑ ▷ Q (LitV true)) →
-  (n2 < n1 → P ⊑ ▷ Q (LitV false)) →
-  P ⊑ wp E ('n1 ≤ 'n2) Q.
-Proof.
-  intros. rewrite -wp_bin_op //; [].
-  destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
-Qed.
-
-Lemma wp_lt E (n1 n2 : nat) P Q :
-  (n1 < n2 → P ⊑ ▷ Q (LitV true)) →
-  (n2 ≤ n1 → P ⊑ ▷ Q (LitV false)) →
-  P ⊑ wp E ('n1 < 'n2) Q.
-Proof.
-  intros. rewrite -wp_bin_op //; [].
-  destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
-Qed.
-
-Lemma wp_eq E (n1 n2 : nat) P Q :
-  (n1 = n2 → P ⊑ ▷ Q (LitV true)) →
-  (n1 ≠ n2 → P ⊑ ▷ Q (LitV false)) →
-  P ⊑ wp E ('n1 = 'n2) Q.
-Proof.
-  intros. rewrite -wp_bin_op //; [].
-  destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
-Qed.
-
-End sugar.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 922e11f4400d02cc85aad87924d8a4af3bd5e01e..b0cd1e7f56d4005ac63cbb0d86818aafe922bda5 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -1,7 +1,7 @@
 (** This file is essentially a bunch of testcases. *)
 Require Import program_logic.ownership.
-Require Import heap_lang.lifting heap_lang.sugar.
-Import heap_lang uPred.
+Require Import heap_lang.notation.
+Import uPred.
 
 Module LangTests.
   Definition add := ('21 + '21)%L.