simp [ofW, toW, toW_ofW (w false), toW_ofW (w true)]
α : Type u_1
isLt✝ : 2 < 3
w : Edge α (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) → WType (Edge α)
⊢ (ofW (WType.mk (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) w)).toW = WType.mk (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) w
α : Type u_1
isLt✝ : 2 < 3
w : Edge α (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w