diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
index 7f52766..08bc166 100644
--- a/src/Quox/Syntax/Var.idr
+++ b/src/Quox/Syntax/Var.idr
@@ -185,6 +185,16 @@ compareP VZ     (VS j) = IsLT LTZ
 compareP (VS i) VZ     = IsGT LTZ
 compareP (VS i) (VS j) = compareS $ compareP i j
 
+export
+0 compareSelf : (c : Compare i i) -> c = IsEQ
+compareSelf (IsLT lt) = absurd lt
+compareSelf IsEQ      = Refl
+compareSelf (IsGT gt) = absurd gt
+
+export
+0 comparePSelf : (i : Var n) -> compareP i i = IsEQ
+comparePSelf i = compareSelf {}
+
 
 public export
 data LTE : Var n -> Var n -> Type where