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 μ
f✝ : Edge L μ (false, Sum.inr (Sum.inl ())) → WType (Edge L μ)
⊢ (ofW (WType.mk (false, Sum.inr (Sum.inl ())) f✝)).toW = WType.mk (false, Sum.inr (Sum.inl ())) f✝
no goals