diff --git a/exercises/compatibility.v b/exercises/compatibility.v
index d103157d9dcb41e88e617747f164885762288a9e..88b86169ab67f7c07612ffae6fb1e66989b5917d 100644
--- a/exercises/compatibility.v
+++ b/exercises/compatibility.v
@@ -18,7 +18,7 @@ is replaced semantic typing judgment in syntactic typing rules. For instance
 becomes:
 
 <<
-  (Γ ⊨ e1 : A1) -∗ (Γ ⊨ e2 : A2) -∗ Γ ⊢ (e1, e2) : A1 * A2
+  (Γ ⊨ e1 : A1) -∗ (Γ ⊨ e2 : A2) -∗ Γ ⊨ (e1, e2) : A1 * A2
 >>
 *)
 
diff --git a/solutions/compatibility.v b/solutions/compatibility.v
index b4fcd8c15e8e2abb93a066e903adcc97a161ad5f..ebea076ad9dc42f1c9d270b8782ea5628ea19c55 100644
--- a/solutions/compatibility.v
+++ b/solutions/compatibility.v
@@ -18,7 +18,7 @@ is replaced semantic typing judgment in syntactic typing rules. For instance
 becomes:
 
 <<
-  (Γ ⊨ e1 : A1) -∗ (Γ ⊨ e2 : A2) -∗ Γ ⊢ (e1, e2) : A1 * A2
+  (Γ ⊨ e1 : A1) -∗ (Γ ⊨ e2 : A2) -∗ Γ ⊨ (e1, e2) : A1 * A2
 >>
 *)