diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 70f53a24b534053d1bb081b88fc4b8b0832e3cf4..12d3c18c0943c8d45c8aa3fdd6aba341c54d01b4 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -11,8 +11,8 @@ Definition par {X} : expr X :=
 Notation Par e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
 Infix "||" := Par : expr_scope.
 
-Instance do_wexpr_assert {X Y} (H : X `included` Y) : WExpr H par par := _.
-Instance do_wsubst_assert {X Y} x es (H : X `included` x :: Y) :
+Instance do_wexpr_par {X Y} (H : X `included` Y) : WExpr H par par := _.
+Instance do_wsubst_par {X Y} x es (H : X `included` x :: Y) :
   WSubst x es H par par := do_wsubst_closed _ x es H _.
 Typeclasses Opaque par.