simp[ofW, toW, toW_ofW (w ())]
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 μ
w : Edge L μ (true, Sum.inr (Sum.inr (Sum.inr ()))) → WType (Edge L μ)
⊢ (ofW (WType.mk (true, Sum.inr (Sum.inr (Sum.inr ()))) w)).toW = WType.mk (true, Sum.inr (Sum.inr (Sum.inr ()))) w
no goals