diff --git a/main.ml b/main.ml
index f982e23..cb9e6b7 100644
--- a/main.ml
+++ b/main.ml
@@ -65,6 +65,15 @@ while !subgoals <> [] do
     let (ty, hyps) = List.hd !subgoals in
     subgoals := List.tl !subgoals;
 
+    let find_hyp (var: var_lambda) : ty option =
+        let rec explore = function
+          | [] -> None
+          | (var_hyp, hyp) :: hyps when var_hyp = var -> Some hyp
+          | _ :: hyps -> explore hyps
+        in
+        explore hyps
+    in
+
     if is_interactive then (
         (* Nettoyage du terminal *)
         let _ = Sys.command("clear -x") in
@@ -120,27 +129,21 @@ while !subgoals <> [] do
             explore hyps
         )
       | Apply var -> (
-            let rec explore = function
-              | (var_hyp, TImpl (t1, t2)) :: _ when var_hyp = var && t2 = ty -> (
+            match find_hyp var with
+              | Some (TImpl (t1, t2)) when t2 = ty -> (
                     subgoals := (t1, hyps) :: !subgoals;
                     fill_holes := function
-                      | hole :: holes -> f ((LApp (LVar var_hyp, hole)) :: holes)
+                      | hole :: holes -> f ((LApp (LVar var, hole)) :: holes)
                       | [] -> fail ()
                 )
-              | [] -> failwith ("Hypothesis " ^ var ^ " not found or unusable")
-              | _ :: hyps -> explore hyps
-            in
-            explore hyps;
+              | None -> failwith ("Hypothesis " ^ var ^ " not found")
+              | _ -> failwith ("Hypothesis " ^ var ^ " unusable")
         )
       | Elim var -> (
-            let rec explore = function
-              | (var_hyp, ty_hyp) :: _ when var_hyp = var && ty_hyp = TFalse -> (
-                    fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes)
-                )
-              | [] -> failwith ("Hypothesis " ^ var ^ " not found or unusable")
-              | _ :: hyps -> explore hyps
-            in
-            explore hyps;
+            match find_hyp var with
+              | Some TFalse -> fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes)
+              | None -> failwith ("Hypothesis " ^ var ^ " not found")
+              | _ -> failwith ("Hypothesis " ^ var ^ " unusable")
         )
 done;