diff --git a/Core.agda b/Core.agda
index bbeee85..aeb2598 100644
--- a/Core.agda
+++ b/Core.agda
@@ -59,10 +59,6 @@ data Desc {i b} {ι : Level i} (I : Type ι) (β : Level b) : Set where
       -> (A : Univ α) -> (⟦ A ⟧ -> Desc I β) -> Desc I β
   _⊛_ : Desc I β -> Desc I β -> Desc I β
 
-_⇨_ : ∀ {i a b} {ι : Level i} {α : Level a} {β : Level b} {I : Type ι} .{{_ : a ≤ₘ b}}
-     -> (A : Univ α) -> Desc I β -> Desc I β
-A ⇨ D = π A λ _ -> D
-
 ⟦_⟧ᵈ : ∀ {i a} {ι : Level i} {α : Level a} {I : Type ι}
      -> Desc I α -> (⟦ I ⟧ -> Set) -> Set
 ⟦ var i ⟧ᵈ B = B i
@@ -91,6 +87,10 @@ knot : ∀ {i a} {ι : Level i} {α : Level a} {I : Type ι} {D : Desc I α} {j}
      -> μ D j -> Extend D (μ D) j
 knot (node e) = e
 
+_⇨_ : ∀ {i a b} {ι : Level i} {α : Level a} {β : Level b} {I : Type ι} .{{_ : a ≤ₘ b}}
+    -> Univ α -> Desc I β -> Desc I β
+A ⇨ D = π A λ _ -> D
+
 data Univ where
   bot  : Prop
   top  : Prop
diff --git a/Lib/Decidable.agda b/Lib/Decidable.agda
index c7e7476..fe8602a 100644
--- a/Lib/Decidable.agda
+++ b/Lib/Decidable.agda
@@ -69,3 +69,15 @@ dhcong₂ : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : Set γ} {x₁ x
         -> f x₁ y₁ # f x₂ y₂
 dhcong₂ f inj (yes refl) q = dcong (f _) (homo ∘ inj) (q _)
 dhcong₂ f inj (no c)     q = no (c ∘ inds ∘ inj)
+
+,-inj : ∀ {α β} {A : Set α} {B : A -> Set β} {x₁ x₂} {y₁ : B x₁} {y₂ : B x₂}
+      -> (x₁ , y₁) ≡ (x₂ , y₂) -> [ B ] y₁ ≅ y₂
+,-inj refl = irefl
+
+_<,>ᵈ_ : ∀ {α β} {A : Set α} {B : Set β} {x₁ x₂ : A} {y₁ y₂ : B}
+       -> x₁ # x₂ -> y₁ # y₂ -> x₁ , y₁ # x₂ , y₂
+_<,>ᵈ_ = dcong₂ _,_ (inds-homo ∘ ,-inj)
+
+_<,>ᵈⁱ_ : ∀ {α β} {A : Set α} {B : A -> Set β} {x₁ x₂} {y₁ : B x₁} {y₂ : B x₂}
+        -> x₁ # x₂ -> (∀ y₂ -> y₁ # y₂) -> x₁ , y₁ # x₂ , y₂
+_<,>ᵈⁱ_ = dhcong₂ _,_ ,-inj
diff --git a/Prelude.agda b/Prelude.agda
index 9721d37..5798071 100644
--- a/Prelude.agda
+++ b/Prelude.agda
@@ -36,18 +36,6 @@ instance
 pright : ∀ {α} {A : Set α} {x y z : A} -> x ≡ y -> x ≡ z -> y ≡ z
 pright prefl prefl = prefl
 
-,-inj : ∀ {α β} {A : Set α} {B : A -> Set β} {x₁ x₂} {y₁ : B x₁} {y₂ : B x₂}
-      -> (x₁ , y₁) ≡ (x₂ , y₂) -> [ B ] y₁ ≅ y₂
-,-inj prefl = irefl
-
-_<,>ᵈ_ : ∀ {α β} {A : Set α} {B : Set β} {x₁ x₂ : A} {y₁ y₂ : B}
-       -> x₁ # x₂ -> y₁ # y₂ -> x₁ , y₁ # x₂ , y₂
-_<,>ᵈ_ = dcong₂ _,_ (inds-homo ∘ ,-inj)
-
-_<,>ᵈᵒ_ : ∀ {α β} {A : Set α} {B : A -> Set β} {x₁ x₂} {y₁ : B x₁} {y₂ : B x₂}
-        -> x₁ # x₂ -> (∀ y₂ -> y₁ # y₂) -> x₁ , y₁ # x₂ , y₂
-_<,>ᵈᵒ_ = dhcong₂ _,_ ,-inj
-
 record Apply {α β} {A : Set α} (B : A -> Set β) x : Set β where
   constructor tag
   field detag : B x
diff --git a/Property/Eq.agda b/Property/Eq.agda
index 9f9471b..8ea3f07 100644
--- a/Property/Eq.agda
+++ b/Property/Eq.agda
@@ -50,7 +50,7 @@ mutual
             -> (D : Desc I α) {{eqD : ExtendEq D}} -> IsSet (Extend D (μ D₀) j)
   decExtend (var i)                q₁        q₂       = yes contr
   decExtend (π A D) {{eqA , eqD}} (x₁ , e₁) (x₂ , e₂) =
-    _≟_ {{eqA}} x₁ x₂ <,>ᵈᵒ decExtend (D x₁) {{apply eqD x₁}} e₁
+    _≟_ {{eqA}} x₁ x₂ <,>ᵈⁱ decExtend (D x₁) {{apply eqD x₁}} e₁
   decExtend (D ⊛ E) {{eqD , eqE}} (s₁ , e₁) (s₂ , e₂) =
     decSem D {{eqD}} s₁ s₂ <,>ᵈ decExtend E {{eqE}} e₁ e₂
 
@@ -66,7 +66,7 @@ mutual
   _≟_ {A = enum n  }               (tag e₁)  (tag e₂)  = dcong tag tag-inj (decEnum n e₁ e₂)
   _≟_ {A = univ α  } {{()}}
   _≟_ {A = σ A B   } {{eqA , eqB}} (x₁ , y₁) (x₂ , y₂) =
-    _≟_ {{eqA}} x₁ x₂ <,>ᵈᵒ _≟_ {{apply eqB x₁}} y₁
+    _≟_ {{eqA}} x₁ x₂ <,>ᵈⁱ _≟_ {{apply eqB x₁}} y₁
   _≟_ {A = π A B   } {{()}}
   _≟_ {A = desc I α} {{()}}
   _≟_ {A = imu D j }                d₁        d₂       = decMu d₁ d₂
diff --git a/readme.md b/readme.md
index 29f4f61..ae11a84 100644
--- a/readme.md
+++ b/readme.md
@@ -4,7 +4,7 @@ It's an implementation of Observational Type Theory as an Agda library. The univ
 
 ## Details
 
-(The readme is a bit old: a `Level` now fully reifies the corresponding `MetaLevel` and there is also a [generic machinery](https://github.com/effectfully/OTT/blob/master/Function/Elim.agda) which allows to derive intensional-type-theory-like eliminators which is annoying to do by hand when a data type is indexed and you need to explicitly use `J`)
+(The readme is a bit old: a `Level` now fully reifies the corresponding `MetaLevel` and there is also a [generic machinery](https://github.com/effectfully/OTT/blob/master/Function/Elim.agda) which allows to derive intensional-type-theory-like eliminators which is annoying to do by hand when a data type is indexed so you need to explicitly use `J`)
 
 There are two main kinds of universe levels (there is also yet another one, but it's not important): metatheory levels (the usual `Level` type renamed to `MetaLevel`) and target theory levels, indexed by metalevels: