diff --git a/_CoqProject b/_CoqProject
index 1c6bf74ca80877a9eeb8858e30a552b7395cc1c1..6690568af2e86fe5e20a458291ced7edb3d328ad 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -38,6 +38,7 @@ theories/bi/bi.v
 theories/bi/tactics.v
 theories/bi/monpred.v
 theories/bi/embedding.v
+theories/bi/weakestpre.v
 theories/bi/lib/counter_examples.v
 theories/bi/lib/fixpoint.v
 theories/bi/lib/fractional.v
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 38671e22036e0fa707fc9333650fc62e95c4ae5d..eb689f8e6d73a02541e2e8963cf9ed35ce1739fd 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -35,7 +35,7 @@
   Σ : gFunctors
   H : heapG Σ
   fun1, fun2, fun3 : expr
-  Φ : language.val heap_lang → iProp Σ
+  Φ : language.val heap_lang → iPropI Σ
   ============================
   --------------------------------------∗
   WP let: "val1" := fun1 #() in
@@ -48,7 +48,7 @@
   Σ : gFunctors
   H : heapG Σ
   fun1, fun2, fun3 : expr
-  Φ : language.val heap_lang → iProp Σ
+  Φ : language.val heap_lang → iPropI Σ
   E : coPset
   ============================
   --------------------------------------∗
diff --git a/theories/bi/weakestpre.v b/theories/bi/weakestpre.v
new file mode 100644
index 0000000000000000000000000000000000000000..212476324febc18f3015853e5f19fef1df2f22dc
--- /dev/null
+++ b/theories/bi/weakestpre.v
@@ -0,0 +1,241 @@
+From stdpp Require Export coPset.
+From iris.program_logic Require Import language.
+From iris.bi Require Import interface derived_connectives.
+
+Inductive stuckness := NotStuck | MaybeStuck.
+
+Definition stuckness_leb (s1 s2 : stuckness) : bool :=
+  match s1, s2 with
+  | MaybeStuck, NotStuck => false
+  | _, _ => true
+  end.
+Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
+Instance stuckness_le_po : PreOrder stuckness_le.
+Proof. split; by repeat intros []. Qed.
+
+Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
+  if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
+
+(** Weakest preconditions [WP e @ s ; E {{ Φ }}] have an additional argument [s]
+of arbitrary type [A], that can be chosen by the one instantiating the [Wp] type
+class. This argument can be used for e.g. the stuckness bit (as in Iris) or
+thread IDs (as in iGPS).
+
+For the case of stuckness bits, there are two specific notations
+[WP e @ E {{ Φ }}] and [WP e @ E ?{{ Φ }}], which forces [A] to be [stuckness],
+and [s] to be [NotStuck] or [MaybeStuck]. *)
+Class Wp (Λ : language) (PROP A : Type) :=
+  wp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
+Arguments wp {_ _ _ _} _ _ _%E _%I.
+Instance: Params (@wp) 7.
+
+Class Twp (Λ : language) (PROP A : Type) :=
+  twp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
+Arguments twp {_ _ _ _} _ _ _%E _%I.
+Instance: Params (@twp) 7.
+
+(** Notations for partial weakest preconditions *)
+(** Notations without binder -- only parsing because they overlap with the
+notations with binder. *)
+Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+
+(** Notations with binder.  The indentation for the inner format block is chosen
+such that *if* one has a single-character mask (e.g. [E]), the second line
+should align with the binder(s) on the first line. *)
+Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' '[          ' @  s ;  E  {{  v ,  Q  } } ']' ']'") : bi_scope.
+Notation "'WP' e @ E {{ v , Q } }" := (wp NotStuck E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' '[       ' @  E  {{  v ,  Q  } } ']' ']'") : bi_scope.
+Notation "'WP' e @ E ? {{ v , Q } }" := (wp MaybeStuck E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' '[        ' @  E  ? {{  v ,  Q  } } ']' ']'") : bi_scope.
+Notation "'WP' e {{ v , Q } }" := (wp NotStuck ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' '[   ' {{  v ,  Q  } } ']' ']'") : bi_scope.
+Notation "'WP' e ? {{ v , Q } }" := (wp MaybeStuck ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' '[    ' ? {{  v ,  Q  } } ']' ']'") : bi_scope.
+
+(* Texan triples *)
+Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ,
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I
+    (at level 20, x closed binder, y closed binder,
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  s ;  E  {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
+Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ,
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I
+    (at level 20, x closed binder, y closed binder,
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  E  {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
+Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ,
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})%I
+    (at level 20, x closed binder, y closed binder,
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  E  ? {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
+Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ,
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})%I
+    (at level 20, x closed binder, y closed binder,
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
+Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ,
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})%I
+    (at level 20, x closed binder, y closed binder,
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' ? {{{  x  ..  y ,   RET  pat ;  Q  } } } ']'") : bi_scope.
+
+Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I
+    (at level 20,
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  s ;  E  {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
+Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I
+    (at level 20,
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  E  {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
+Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})%I
+    (at level 20,
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  E  ? {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
+Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I
+    (at level 20,
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
+Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})%I
+    (at level 20,
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' ? {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
+
+(** Aliases for stdpp scope -- they inherit the levels and format from above. *)
+Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
+Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
+Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
+Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }}) : stdpp_scope.
+Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }}) : stdpp_scope.
+Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
+  (∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
+Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
+  (∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
+Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
+  (∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
+Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
+  (∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }}) : stdpp_scope.
+Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
+  (∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }}) : stdpp_scope.
+
+(** Notations for total weakest preconditions *)
+(** Notations without binder -- only parsing because they overlap with the
+notations with binder. *)
+Notation "'WP' e @ s ; E [{ Φ } ]" := (twp s E e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+Notation "'WP' e @ E [{ Φ } ]" := (twp NotStuck E e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+Notation "'WP' e @ E ? [{ Φ } ]" := (twp MaybeStuck E e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+Notation "'WP' e [{ Φ } ]" := (twp NotStuck ⊤ e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+Notation "'WP' e ? [{ Φ } ]" := (twp MaybeStuck ⊤ e%E Φ)
+  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
+
+(** Notations with binder.  The indentation for the inner format block is chosen
+such that *if* one has a single-character mask (e.g. [E]), the second line
+should align with the binder(s) on the first line. *)
+Notation "'WP' e @ s ; E [{ v , Q } ]" := (twp s E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' '[          ' @  s ;  E  [{  v ,  Q  } ] ']' ']'") : bi_scope.
+Notation "'WP' e @ E [{ v , Q } ]" := (twp NotStuck E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' '[       ' @  E  [{  v ,  Q  } ] ']' ']'") : bi_scope.
+Notation "'WP' e @ E ? [{ v , Q } ]" := (twp MaybeStuck E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' '[        ' @  E  ? [{  v ,  Q  } ] ']' ']'") : bi_scope.
+Notation "'WP' e [{ v , Q } ]" := (twp NotStuck ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' '[   ' [{  v ,  Q  } ] ']' ']'") : bi_scope.
+Notation "'WP' e ? [{ v , Q } ]" := (twp MaybeStuck ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' '[    ' ? [{  v ,  Q  } ] ']' ']'") : bi_scope.
+
+(* Texan triples *)
+Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' @  s ;  E  [[{  x  ..  y ,  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' @  E  [[{  x  ..  y ,  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+Notation "'[[{' P } ] ] e @ E ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?[{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' @  E  ? [[{  x  ..  y ,  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' [[{  x  ..  y ,  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+Notation "'[[{' P } ] ] e ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?[{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' ? [[{  x  ..  y ,   RET  pat ;  Q  } ] ] ']'") : bi_scope.
+
+Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }])%I
+    (at level 20,
+     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' @  s ;  E  [[{  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }])%I
+    (at level 20,
+     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' @  E  [[{  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E ?[{ Φ }])%I
+    (at level 20,
+     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' @  E  ? [[{  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }])%I
+    (at level 20,
+     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' [[{  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e ?[{ Φ }])%I
+    (at level 20,
+     format "'[hv' [[{  P  } ] ]  '/  ' e  '/' ? [[{  RET  pat ;  Q  } ] ] ']'") : bi_scope.
+
+(** Aliases for stdpp scope -- they inherit the levels and format from above. *)
+Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?[{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?[{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E ?[{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }]) : stdpp_scope.
+Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e ?[{ Φ }]) : stdpp_scope.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index d782a858abeac9401ef567ef09e177e370350656..ddc60dc414be6a79c9b79768d4e84558a2984ebd 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -50,142 +50,13 @@ Qed.
 Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset)
     (e : expr Λ) (Φ : val Λ → iProp Σ) :
   iProp Σ := bi_least_fixpoint (twp_pre' s) (E,e,Φ).
-Definition twp_aux : seal (@twp_def). by eexists. Qed.
-Definition twp := twp_aux.(unseal).
-Definition twp_eq : @twp = @twp_def := twp_aux.(seal_eq).
-
-Arguments twp {_ _ _} _ _ _%E _.
-Instance: Params (@twp) 6.
-
-(* Note that using '[[' instead of '[{' results in conflicts with the list
-notations. *)
-Notation "'WP' e @ s ; E [{ Φ } ]" := (twp s E e%E Φ)
-  (at level 20, e, Φ at level 200,
-   format "'[' 'WP'  e  '/' @  s ;  E  [{  Φ  } ] ']'") : bi_scope.
-Notation "'WP' e @ E [{ Φ } ]" := (twp NotStuck E e%E Φ)
-  (at level 20, e, Φ at level 200,
-   format "'[' 'WP'  e  '/' @  E  [{  Φ  } ] ']'") : bi_scope.
-Notation "'WP' e @ E ? [{ Φ } ]" := (twp MaybeStuck E e%E Φ)
-  (at level 20, e, Φ at level 200,
-   format "'[' 'WP'  e  '/' @  E  ? [{  Φ  } ] ']'") : bi_scope.
-Notation "'WP' e [{ Φ } ]" := (twp NotStuck ⊤ e%E Φ)
-  (at level 20, e, Φ at level 200,
-   format "'[' 'WP'  e  '/' [{  Φ  } ] ']'") : bi_scope.
-Notation "'WP' e ? [{ Φ } ]" := (twp MaybeStuck ⊤ e%E Φ)
-  (at level 20, e, Φ at level 200,
-   format "'[' 'WP'  e  '/' ? [{  Φ  } ] ']'") : bi_scope.
-
-Notation "'WP' e @ s ; E [{ v , Q } ]" := (twp s E e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' @  s ;  E  [{  v ,  Q  } ] ']'") : bi_scope.
-Notation "'WP' e @ E [{ v , Q } ]" := (twp NotStuck E e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' @  E  [{  v ,  Q  } ] ']'") : bi_scope.
-Notation "'WP' e @ E ? [{ v , Q } ]" := (twp MaybeStuck E e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' @  E  ? [{  v ,  Q  } ] ']'") : bi_scope.
-Notation "'WP' e [{ v , Q } ]" := (twp NotStuck ⊤ e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' [{  v ,  Q  } ] ']'") : bi_scope.
-Notation "'WP' e ? [{ v , Q } ]" := (twp MaybeStuck ⊤ e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' ? [{  v ,  Q  } ] ']'") : bi_scope.
-
-(* Texan triples *)
-Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
-  (□ ∀ Φ,
-      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }])%I
-    (at level 20, x closed binder, y closed binder,
-     format "[[{  P  } ] ]  e  @  s ;  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : bi_scope.
-Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
-  (□ ∀ Φ,
-      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }])%I
-    (at level 20, x closed binder, y closed binder,
-     format "[[{  P  } ] ]  e  @  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : bi_scope.
-Notation "'[[{' P } ] ] e @ E ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
-  (□ ∀ Φ,
-      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?[{ Φ }])%I
-    (at level 20, x closed binder, y closed binder,
-     format "[[{  P  } ] ]  e  @  E  ? [[{  x .. y ,  RET  pat ;  Q } ] ]") : bi_scope.
-Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
-  (□ ∀ Φ,
-      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }])%I
-    (at level 20, x closed binder, y closed binder,
-     format "[[{  P  } ] ]  e  [[{  x .. y ,   RET  pat ;  Q } ] ]") : bi_scope.
-Notation "'[[{' P } ] ] e ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
-  (□ ∀ Φ,
-      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?[{ Φ }])%I
-    (at level 20, x closed binder, y closed binder,
-     format "[[{  P  } ] ]  e  ? [[{  x .. y ,   RET  pat ;  Q } ] ]") : bi_scope.
-Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
-  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }])%I
-    (at level 20,
-     format "[[{  P  } ] ]  e  @  s ;  E  [[{  RET  pat ;  Q } ] ]") : bi_scope.
-Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
-  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }])%I
-    (at level 20,
-     format "[[{  P  } ] ]  e  @  E  [[{  RET  pat ;  Q } ] ]") : bi_scope.
-Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
-  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E ?[{ Φ }])%I
-    (at level 20,
-     format "[[{  P  } ] ]  e  @  E  ? [[{  RET  pat ;  Q } ] ]") : bi_scope.
-Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
-  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }])%I
-    (at level 20,
-     format "[[{  P  } ] ]  e  [[{  RET  pat ;  Q } ] ]") : bi_scope.
-Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
-  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e ?[{ Φ }])%I
-    (at level 20,
-     format "[[{  P  } ] ]  e  ? [[{  RET  pat ;  Q } ] ]") : bi_scope.
-
-Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
-  (∀ Φ : _ → uPred _,
-      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }])
-    (at level 20, x closed binder, y closed binder,
-     format "[[{  P  } ] ]  e  @  s ;  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
-Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
-  (∀ Φ : _ → uPred _,
-      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }])
-    (at level 20, x closed binder, y closed binder,
-     format "[[{  P  } ] ]  e  @  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
-Notation "'[[{' P } ] ] e @ E ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
-  (∀ Φ : _ → uPred _,
-      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?[{ Φ }])
-    (at level 20, x closed binder, y closed binder,
-     format "[[{  P  } ] ]  e  @  E  ? [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
-Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
-  (∀ Φ : _ → uPred _,
-      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }])
-    (at level 20, x closed binder, y closed binder,
-     format "[[{  P  } ] ]  e  [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
-Notation "'[[{' P } ] ] e ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
-  (∀ Φ : _ → uPred _,
-      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?[{ Φ }])
-    (at level 20, x closed binder, y closed binder,
-     format "[[{  P  } ] ]  e  ? [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
-Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
-  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }])
-    (at level 20,
-     format "[[{  P  } ] ]  e  @  s ;  E  [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
-Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
-  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }])
-    (at level 20,
-     format "[[{  P  } ] ]  e  @  E  [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
-Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
-  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E ?[{ Φ }])
-    (at level 20,
-     format "[[{  P  } ] ]  e  @  E  ? [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
-Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
-  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }])
-    (at level 20,
-     format "[[{  P  } ] ]  e  [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
-Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
-  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e ?[{ Φ }])
-    (at level 20,
-     format "[[{  P  } ] ]  e  ? [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
+Definition twp_aux `{irisG Λ Σ} : seal (@twp_def Λ Σ _). by eexists. Qed.
+Instance twp' `{irisG Λ Σ} : Twp Λ (iProp Σ) stuckness := twp_aux.(unseal).
+Definition twp_eq `{irisG Λ Σ} : twp = @twp_def Λ Σ _ := twp_aux.(seal_eq).
 
 Section twp.
 Context `{irisG Λ Σ}.
+Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
@@ -210,12 +81,12 @@ Proof.
 Qed.
 
 Global Instance twp_ne s E e n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@twp Λ Σ _ s E e).
+  Proper (pointwise_relation _ (dist n) ==> dist n) (twp (PROP:=iProp Σ) s E e).
 Proof.
   intros Φ1 Φ2 HΦ. rewrite !twp_eq. by apply (least_fixpoint_ne _), pair_ne, HΦ.
 Qed.
 Global Instance twp_proper s E e :
-  Proper (pointwise_relation _ (≡) ==> (≡)) (@twp Λ Σ _ s E e).
+  Proper (pointwise_relation _ (≡) ==> (≡)) (twp (PROP:=iProp Σ) s E e).
 Proof.
   by intros Φ Φ' ?; apply equiv_dist=>n; apply twp_ne=>v; apply equiv_dist.
 Qed.
@@ -339,7 +210,7 @@ Lemma twp_mask_mono s E1 E2 e Φ :
   E1 ⊆ E2 → WP e @ s; E1 [{ Φ }] -∗ WP e @ s; E2 [{ Φ }].
 Proof. iIntros (?) "H"; iApply (twp_strong_mono with "H"); auto. Qed.
 Global Instance twp_mono' s E e :
-  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@twp Λ Σ _ s E e).
+  Proper (pointwise_relation _ (⊢) ==> (⊢)) (twp (PROP:=iProp Σ) s E e).
 Proof. by intros Φ Φ' ?; apply twp_mono. Qed.
 
 Lemma twp_value s E Φ e v `{!IntoVal e v} : Φ v -∗ WP e @ s; E [{ Φ }].
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 19934800d69a260eea91fdb1711832165f4097b2..20e1945f29cd7073a5ff8899d883dd4fd8058f4f 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -1,5 +1,6 @@
 From iris.base_logic.lib Require Export fancy_updates.
 From iris.program_logic Require Export language.
+From iris.bi Require Export weakestpre.
 From iris.proofmode Require Import tactics classes.
 Set Default Proof Using "Type".
 Import uPred.
@@ -11,20 +12,6 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
 Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 Global Opaque iris_invG.
 
-Inductive stuckness := NotStuck | MaybeStuck.
-
-Definition stuckness_leb (s1 s2 : stuckness) : bool :=
-  match s1, s2 with
-  | MaybeStuck, NotStuck => false
-  | _, _ => true
-  end.
-Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
-Instance stuckness_le_po : PreOrder stuckness_le.
-Proof. split; by repeat intros []. Qed.
-
-Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
-  if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
-
 Definition wp_pre `{irisG Λ Σ} (s : stuckness)
     (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
     coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
@@ -45,119 +32,9 @@ Qed.
 
 Definition wp_def `{irisG Λ Σ} (s : stuckness) :
   coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
-Definition wp_aux : seal (@wp_def). by eexists. Qed.
-Definition wp := wp_aux.(unseal).
-Definition wp_eq : @wp = @wp_def := wp_aux.(seal_eq).
-
-Arguments wp {_ _ _} _ _ _%E _.
-Instance: Params (@wp) 6.
-
-(* Notations without binder -- only parsing because they overlap with the
-notations with binder. *)
-Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e%E Φ)
-  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
-Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e%E Φ)
-  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
-Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e%E Φ)
-  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
-Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ)
-  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
-Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ e%E Φ)
-  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
-
-(* Notations with binder.  The indentation for the inner format block is chosen
-such that *if* one has a single-character mask (e.g. [E]), the second line
-should align with the binder(s) on the first line. *)
-Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[          ' @  s ;  E  {{  v ,  Q  } } ']' ']'") : bi_scope.
-Notation "'WP' e @ E {{ v , Q } }" := (wp NotStuck E e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[       ' @  E  {{  v ,  Q  } } ']' ']'") : bi_scope.
-Notation "'WP' e @ E ? {{ v , Q } }" := (wp MaybeStuck E e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[        ' @  E  ? {{  v ,  Q  } } ']' ']'") : bi_scope.
-Notation "'WP' e {{ v , Q } }" := (wp NotStuck ⊤ e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[   ' {{  v ,  Q  } } ']' ']'") : bi_scope.
-Notation "'WP' e ? {{ v , Q } }" := (wp MaybeStuck ⊤ e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' '[    ' ? {{  v ,  Q  } } ']' ']'") : bi_scope.
-
-(* Texan triples *)
-Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
-  (□ ∀ Φ,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I
-    (at level 20, x closed binder, y closed binder,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  s ;  E  {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
-Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
-  (□ ∀ Φ,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I
-    (at level 20, x closed binder, y closed binder,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  E  {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
-Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
-  (□ ∀ Φ,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})%I
-    (at level 20, x closed binder, y closed binder,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  E  ? {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
-Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
-  (□ ∀ Φ,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})%I
-    (at level 20, x closed binder, y closed binder,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
-Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
-  (□ ∀ Φ,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})%I
-    (at level 20, x closed binder, y closed binder,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' ? {{{  x  ..  y ,   RET  pat ;  Q  } } } ']'") : bi_scope.
-
-Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
-  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I
-    (at level 20,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  s ;  E  {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
-Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
-  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I
-    (at level 20,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  E  {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
-Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
-  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})%I
-    (at level 20,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' @  E  ? {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
-Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
-  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I
-    (at level 20,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
-Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
-  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})%I
-    (at level 20,
-     format "'[hv' {{{  P  } } }  '/  ' e  '/' ? {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
-
-(* Aliases for stdpp scope -- they inherit the levels and format from above. *)
-Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
-Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
-Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
-Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }}) : stdpp_scope.
-Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }}) : stdpp_scope.
-Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
-Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
-Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
-Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }}) : stdpp_scope.
-Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }}) : stdpp_scope.
+Definition wp_aux `{irisG Λ Σ} : seal (@wp_def Λ Σ _). by eexists. Qed.
+Instance wp' `{irisG Λ Σ} : Wp Λ (iProp Σ) stuckness := wp_aux.(unseal).
+Definition wp_eq `{irisG Λ Σ} : wp = @wp_def Λ Σ _ := wp_aux.(seal_eq).
 
 Section wp.
 Context `{irisG Λ Σ}.
@@ -168,11 +45,12 @@ Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 
 (* Weakest pre *)
-Lemma wp_unfold s E e Φ : WP e @ s; E {{ Φ }} ⊣⊢ wp_pre s (wp s) E e Φ.
+Lemma wp_unfold s E e Φ :
+  WP e @ s; E {{ Φ }} ⊣⊢ wp_pre s (wp (PROP:=iProp Σ)  s) E e Φ.
 Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre s)). Qed.
 
 Global Instance wp_ne s E e n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ s E e).
+  Proper (pointwise_relation _ (dist n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
 Proof.
   revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
   rewrite !wp_unfold /wp_pre.
@@ -183,7 +61,7 @@ Proof.
   intros v. eapply dist_le; eauto with omega.
 Qed.
 Global Instance wp_proper s E e :
-  Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ _ s E e).
+  Proper (pointwise_relation _ (≡) ==> (≡)) (wp (PROP:=iProp Σ) s E e).
 Proof.
   by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
 Qed.
@@ -294,7 +172,7 @@ Proof. apply wp_stuck_mono. by destruct s. Qed.
 Lemma wp_mask_mono s E1 E2 e Φ : E1 ⊆ E2 → WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Φ }}.
 Proof. iIntros (?) "H"; iApply (wp_strong_mono with "H"); auto. Qed.
 Global Instance wp_mono' s E e :
-  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ _ s E e).
+  Proper (pointwise_relation _ (⊢) ==> (⊢)) (wp (PROP:=iProp Σ) s E e).
 Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
 
 Lemma wp_value s E Φ e v `{!IntoVal e v} : Φ v ⊢ WP e @ s; E {{ Φ }}.
@@ -411,5 +289,4 @@ Section proofmode_classes.
     iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
     iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
   Qed.
-
 End proofmode_classes.