diff --git a/tests/mosel_paper.ref b/tests/mosel_paper.ref
index 3031fbef6daf6da4f7add50dd373d6ca753f5d29..700e1159a429303df2d04f7dd27d6ef515796122 100644
--- a/tests/mosel_paper.ref
+++ b/tests/mosel_paper.ref
@@ -10,7 +10,7 @@
   --------------------------------------∗
   ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
   
-2 subgoals
+1 subgoal
   
   PROP : bi
   A : Type
@@ -23,13 +23,19 @@
   --------------------------------------∗
   ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
   
-
-subgoal 2 is:
- "HP" : P
-"H2" : Ψ x
---------------------------------------∗
-∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
-
+1 subgoal
+  
+  PROP : bi
+  A : Type
+  P : PROP
+  Φ, Ψ : A → PROP
+  x : A
+  ============================
+  "HP" : P
+  "H2" : Ψ x
+  --------------------------------------∗
+  ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
+  
 1 subgoal
   
   PROP : bi
diff --git a/tests/mosel_paper.v b/tests/mosel_paper.v
index e5e08f8c44e7fa80b453afdc870c8875cd503542..25211740a8f9c6cf244641c542422e59dbe31abe 100644
--- a/tests/mosel_paper.v
+++ b/tests/mosel_paper.v
@@ -12,9 +12,9 @@ Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
   P ∗ (∃ a, Φ a ∨ Ψ a) -∗ ∃ a, (P ∗ Φ a) ∨ (P ∗ Ψ a).
 Proof.
   iIntros "[HP H]". Show.
-  iDestruct "H" as (x) "[H1|H2]". Show.
-  - iExists x. iLeft. iSplitL "HP"; iAssumption.
-  - iExists x. iRight. iSplitL "HP"; iAssumption.
+  iDestruct "H" as (x) "[H1|H2]".
+  - Show. iExists x. iLeft. iSplitL "HP"; iAssumption.
+  - Show. iExists x. iRight. iSplitL "HP"; iAssumption.
 Qed.
 Lemma example {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
 P ∗ (∃ a, Φ a ∨ Ψ a) -∗ ∃ a, (P ∗ Φ a) ∨ (P ∗ Ψ a).