diff --git a/src/logic/hydra.lean b/src/logic/hydra.lean
index 97260914248eb..286d1a2434a9a 100644
--- a/src/logic/hydra.lean
+++ b/src/logic/hydra.lean
@@ -136,7 +136,8 @@ begin
 end
 
 /-- `cut_expand r` is well-founded when `r` is. -/
-theorem _root_.well_founded.cut_expand (hr : well_founded r) : well_founded (cut_expand r) :=
-⟨by { letI h := hr.is_irrefl, exact λ s, acc_of_singleton $ λ a _, (hr.apply a).cut_expand }⟩
+instance _root_.is_well_founded.cut_expand [is_well_founded α r] :
+  is_well_founded _ (cut_expand r) :=
+⟨⟨λ s, acc_of_singleton $ λ a _, (is_well_founded.apply r a).cut_expand⟩⟩
 
 end relation