diff --git a/base/src/test/resources/failure/holes/issue747.aya.txt b/base/src/test/resources/failure/holes/issue747.aya.txt
index 1c62c2cba9..c6518135ef 100644
--- a/base/src/test/resources/failure/holes/issue747.aya.txt
+++ b/base/src/test/resources/failure/holes/issue747.aya.txt
@@ -11,7 +11,7 @@ Goal: Goal of type
       Context:
         {a : Nat}
       To ensure confluence:
-        Given (i ⇒ _), we should have: 0
+        Given (_ ⇒ 0, i ⇒ _), we should have: 0
 
 In file $FILE:11:13 ->
 
diff --git a/base/src/test/resources/success/src/Prop.aya b/base/src/test/resources/success/src/Prop.aya
index 3e9b66037e..380478f99e 100644
--- a/base/src/test/resources/success/src/Prop.aya
+++ b/base/src/test/resources/success/src/Prop.aya
@@ -1,3 +1,5 @@
+open import Paths
+
 open struct Squash (A: Type): Prop
   | value: A
 
@@ -9,3 +11,9 @@ def squashElim {A: Type} {P: Prop} (f: A -> P) (squash: Squash A): P => f squash
 def squash2Elim {A: Type} {P: Prop} (f: A -> P) (squash: Squash2 A): P
   | f, (squash a) => f a
 
+open data Carry (A : Prop) : Type
+| carry A
+
+open data Bool : Prop | true | false
+
+def check : carry true = carry false => idp