diff --git a/lexer.mll b/lexer.mll
index e8bfc32..e1d8c5c 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -17,5 +17,6 @@ and token_tactic = parse
   | [' ' '\t' '\n']             { token_tactic lexbuf }
   | eof                         { EOF }
   | "intro"                     { INTRO }
+  | "assumption"                { ASSUMPTION }
   | ['a'-'z']+['0'-'9']* as s   { VAR_NAME s }
   | '.'                         { DOT }
diff --git a/main.ml b/main.ml
index 2d37e46..4240964 100644
--- a/main.ml
+++ b/main.ml
@@ -62,7 +62,7 @@ let subgoals: (ty * (var_lambda * ty) list) list ref = ref [(ty, [])] in
 let fill_holes = ref (fun holes -> List.hd holes) in
 
 while !subgoals <> [] do
-    let (ty, hyp) = List.hd !subgoals in
+    let (ty, hyps) = List.hd !subgoals in
     subgoals := List.tl !subgoals;
 
     if is_interactive then (
@@ -70,7 +70,7 @@ while !subgoals <> [] do
         let _ = Sys.command("clear -x") in
 
         (* Affichage des hypothèses *)
-        List.iter (fun (var, h) -> Printf.printf "%s: %s\n" var (string_of_ty h)) hyp;
+        List.iter (fun (var, h) -> Printf.printf "%s: %s\n" var (string_of_ty h)) hyps;
 
         (* Affichage des sous-buts *)
         Printf.printf "================\n";
@@ -96,18 +96,29 @@ while !subgoals <> [] do
         read_tactic ()
     in
 
+    let f = !fill_holes in
+
     match tactic with
       | Intro var -> (
             match ty with
               | TImpl (ty1, ty2) -> (
-                    subgoals := (ty2, (var, ty1) :: hyp) :: !subgoals;
-                    let f = !fill_holes in
+                    subgoals := (ty2, (var, ty1) :: hyps) :: !subgoals;
                     fill_holes := fun holes -> match holes with
                       | h :: hs -> f (LFun (var, ty1, h) :: hs)
                       | _ -> fail ()
                 )
               | _ -> failwith "Can't intro"
         )
+      | Assumption -> (
+            let rec explore = function
+              | (var, hyp) :: _ when hyp = ty -> (
+                    fill_holes := fun holes -> f ((LVar var) :: holes)
+                )
+              | [] -> failwith "No such hypothesis"
+              | _ :: hyps -> explore hyps
+            in
+            explore hyps
+        )
 done;
 
-Printf.printf "Final proof :\n%s" (string_of_lam (!fill_holes []));;
+Printf.printf "Final proof :\n%s\n" (string_of_lam (!fill_holes []));;
diff --git a/parser.mly b/parser.mly
index 7313935..84d2a16 100644
--- a/parser.mly
+++ b/parser.mly
@@ -10,7 +10,7 @@
 %token <string> VAR_NAME
 %token <string> TYPE_NAME
 
-%token DOT INTRO
+%token DOT INTRO ASSUMPTION
 
 /* L'ordre de définition définit la priorité */
 %right RARROW
@@ -38,3 +38,4 @@ main_tactic:
 
 tactic:
   | INTRO VAR_NAME DOT                    { Intro $2 }
+  | ASSUMPTION DOT                        { Assumption }