apply congr_arg
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 μ
this✝ : (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
this :
  encode (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
⊢ encode
      (WType.SubWType.cast this✝
        (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
          ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯)) =
    encode (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯)
case h
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 μ
this✝ : (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
this :
  encode (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 0 (2 * k.pair ((encode r).pair (encode v)))).pair 0
⊢ WType.SubWType.cast this✝
      (WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    WType.SubWType.ofWType (WType.mk (false, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯