ext b
α : Type u_1
isLt✝ : 1 < 3
w : Edge α (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
case h
α : Type u_1
isLt✝ : 1 < 3
w : Edge α (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) → WType (Edge α)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b