diff --git a/main.ml b/main.ml
index 7e9d411..31bc94e 100644
--- a/main.ml
+++ b/main.ml
@@ -7,13 +7,13 @@ let fail () =
 (* Parsage des arguments*)
 let filename = ref "" in
 
-let reduce = ref false in
-let alpha = ref false in
+let reduce_option = ref false in
+let alpha_option = ref false in
 let typecheck_option = ref false in
 
 Arg.parse
-    [("-reduce", Arg.Set reduce, "Show the step-by-step reduction of a lambda-term");
-     ("-alpha", Arg.Set alpha, "Check is two lambda-terms separated by '&' are alpha-convertible");
+    [("-reduce", Arg.Set reduce_option, "Show the step-by-step reduction of a lambda-term");
+     ("-alpha", Arg.Set alpha_option, "Check is two lambda-terms separated by '&' are alpha-convertible");
      ("-typecheck", Arg.Set typecheck_option, "Check if a lambda term has a given type")]
     (fun s -> filename := s)
     "The available options are:";
@@ -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
@@ -75,6 +84,9 @@ while !subgoals <> [] do
         (* Affichage des sous-buts *)
         Printf.printf "================\n";
         Printf.printf "%s\n" (string_of_ty ty);
+        List.iter (fun (ty, _) ->
+            Printf.printf "%s\n" (string_of_ty ty)
+        ) !subgoals;
 
         (* Lecture d'une tactique *)
         Printf.printf "What do you want to do?\n"
@@ -120,27 +132,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")
         )
       | Cut tint -> (
             subgoals := (TImpl(tint, ty), hyps)::(tint, hyps)::!subgoals;