simp[ofW, toW, Empty.eq_elim]
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 μ
fst✝ : ℕ
r : L.Rel fst✝
v : Fin fst✝ → UTerm L μ
f✝ : Edge L μ (false, Sum.inl ⟨fst✝, (r, v)⟩) → WType (Edge L μ)
⊢ (ofW (WType.mk (false, Sum.inl ⟨fst✝, (r, v)⟩) f✝)).toW = WType.mk (false, Sum.inl ⟨fst✝, (r, v)⟩) f✝
no goals