diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index 123cb18..ca2891f 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -102,7 +102,7 @@ Triangle' a = Context $ Context (\_ => a)
 
 export
 0 telescopeLTE : Telescope _ from to -> from `LTE` to
-telescopeLTE [<]        = reflexive {rel=Nat.LTE}
+telescopeLTE [<]        = reflexive
 telescopeLTE (tel :< _) = lteSuccRight $ telescopeLTE tel
 
 export
@@ -111,7 +111,7 @@ export
 
 export %hint
 0 succGT : S n `GT` n
-succGT = LTESucc $ reflexive {rel=Nat.LTE}
+succGT = LTESucc reflexive
 
 
 parameters {auto _ : Applicative f}
@@ -176,7 +176,7 @@ namespace Nat
 
   export
   lte'ToLte : {n : Nat} -> m `LTE'` n -> m `LTE` n
-  lte'ToLte LTERefl      = reflexive {rel=Nat.LTE}
+  lte'ToLte LTERefl      = reflexive
   lte'ToLte (LTESuccR p) = lteSuccRight (lte'ToLte p)
 
   export
diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr
index 67d3903..2a5969b 100644
--- a/src/Quox/Syntax/Shift.idr
+++ b/src/Quox/Syntax/Shift.idr
@@ -47,7 +47,7 @@ fromEqv (EqSS e) = cong SS $ fromEqv e
 export
 0 toEqv : by = bz -> by `Eqv` bz
 toEqv Refl {by = SZ}      = EqSZ
-toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl {by}
+toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl
 
 
 export
@@ -60,9 +60,9 @@ export
                by.nat + i.nat `LT` to
 shiftVarLT by i =
   rewrite plusSuccRightSucc by.nat i.nat in
-  transitive {rel=Nat.LTE}
+  transitive
     (plusLteMonotoneLeft by.nat (S i.nat) from (toNatLT i))
-    (replace {p=(`LTE` to)} (shiftDiff by) $ reflexive {rel=Nat.LTE})
+    (replace {p=(`LTE` to)} (shiftDiff by) reflexive)
 
 
 public export
@@ -85,7 +85,7 @@ export
 0 toNatInj' : (by : Shift from1 to1) -> (bz : Shift from2 to2) ->
               by.nat = bz.nat -> by `Eqv` bz
 toNatInj' SZ      SZ      prf = EqSZ
-toNatInj' (SS by) (SS bz) prf = EqSS $ toNatInj' by bz $ succInjective _ _ prf
+toNatInj' (SS by) (SS bz) prf = EqSS $ toNatInj' by bz $ injective prf
 toNatInj' (SS by) SZ      Refl impossible
 
 export
diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
index 08bc166..da71b5b 100644
--- a/src/Quox/Syntax/Var.idr
+++ b/src/Quox/Syntax/Var.idr
@@ -105,7 +105,7 @@ toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
 -- to be an instance of <https://github.com/idris-lang/Idris2/issues/1259>?
 export
 weak : (0 p : m `LTE` n) -> Var m -> Var n
-weak p i = fromNatWith i.nat $ transitive (toNatLT i) p {rel=LTE}
+weak p i = fromNatWith i.nat $ transitive (toNatLT i) p
 
 public export
 0 weakSpec : m `LTE` n -> Var m -> Var n
@@ -150,7 +150,7 @@ i `GT` j = j `LT` i
 export
 Transitive (Var n) LT where
   transitive LTZ     (LTS _) = LTZ
-  transitive (LTS p) (LTS q) = LTS $ transitive p q {rel = Var.LT}
+  transitive (LTS p) (LTS q) = LTS $ transitive p q
 
 export Uninhabited (i    `Var.LT` i)  where uninhabited (LTS p) = uninhabited p
 export Uninhabited (VS i `LT`     VZ) where uninhabited _ impossible
@@ -204,17 +204,17 @@ data LTE : Var n -> Var n -> Type where
 export
 Reflexive (Var n) LTE where
   reflexive {x = VZ}   = LTEZ
-  reflexive {x = VS i} = LTES $ reflexive {x = i}
+  reflexive {x = VS i} = LTES reflexive
 
 export
 Transitive (Var n) LTE where
   transitive LTEZ     q        = LTEZ
-  transitive (LTES p) (LTES q) = LTES $ transitive p q {rel = Var.LTE}
+  transitive (LTES p) (LTES q) = LTES $ transitive p q
 
 export
 Antisymmetric (Var n) LTE where
   antisymmetric LTEZ     LTEZ     = Refl
-  antisymmetric (LTES p) (LTES q) = cong VS $ antisymmetric p q {rel = Var.LTE}
+  antisymmetric (LTES p) (LTES q) = cong VS $ antisymmetric p q
 
 export
 splitLTE : {j : Var n} -> i `LTE` j -> Either (i = j) (i `LT` j)