simp[primcodable, Primcodable.ofEquiv_toEncodable,
  Encodable.encode_ofEquiv (equivW L μ), WType.encode_eq, WType.SubWType.ofW, WType.depth]
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
⊢ encode (rel r v) = Nat.pair 1 ((Nat.pair 1 ((2 * k.pair) ((encode r).pair (encode v)))).pair 0)
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
⊢ encode
      (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0