diff --git a/ProofMode.md b/ProofMode.md
index 5a132163c01e6550945194685b02b4fab2043fec..d86362ea802b50ebdf9abede793f4a7d2117c4cb 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -137,13 +137,13 @@ You can write
 
 which results in:
 
-				x : nat
-				H : x = 0
-				______________________________________(1/1)
-				​​"HQ" : Q
-				​"HR" : R
-				--------------------------------------â–¡
-				R ★ Q ∧ x = 1
+        x : nat
+        H : x = 0
+        ______________________________________(1/1)
+				"HQ" : Q
+        "HR" : R
+        --------------------------------------â–¡
+        R ★ Q ∧ x = 1
 
 
 Specialization patterns