diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index e5bba64..38dc637 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -209,6 +209,9 @@ CanSubst (Elim d) (Term d) where
                          Shift SZ => s
                          th       => CloT s th
 
+export CanSubst Var (Term d) where s // th = s // map (B {d}) th
+export CanSubst Var (Elim d) where e // th = e // map (B {d}) th
+
 export CanShift (Term d) where i // by = i // Shift by {env=(Elim d)}
 export CanShift (Elim d) where i // by = i // Shift by {env=(Elim d)}