diff --git a/lexer.mll b/lexer.mll
index e1d8c5c..f6f533a 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -18,5 +18,6 @@ and token_tactic = parse
   | eof                         { EOF }
   | "intro"                     { INTRO }
   | "assumption"                { ASSUMPTION }
+  | "apply"                     { APPLY }
   | ['a'-'z']+['0'-'9']* as s   { VAR_NAME s }
   | '.'                         { DOT }
diff --git a/main.ml b/main.ml
index e62d227..d96472a 100644
--- a/main.ml
+++ b/main.ml
@@ -119,6 +119,19 @@ while !subgoals <> [] do
             in
             explore hyps
         )
+      | Apply var -> (
+            let rec explore = function
+              | (var_hyp, TImpl (t1, t2)) :: _ when var_hyp = var && t2 = ty -> (
+                    subgoals := (t1, hyps) :: !subgoals;
+                    fill_holes := function
+                      | hole :: holes -> f ((LApp (LVar var_hyp, hole)) :: holes)
+                      | [] -> fail ()
+                )
+              | [] -> failwith ("Hypothesis " ^ var ^ " not found or unusable")
+              | _ :: hyps -> explore hyps
+            in
+            explore hyps;
+        )
 done;
 
 let finalLam = !fill_holes [] in
diff --git a/parser.mly b/parser.mly
index 84d2a16..7d52621 100644
--- a/parser.mly
+++ b/parser.mly
@@ -10,7 +10,7 @@
 %token <string> VAR_NAME
 %token <string> TYPE_NAME
 
-%token DOT INTRO ASSUMPTION
+%token DOT INTRO ASSUMPTION APPLY
 
 /* L'ordre de définition définit la priorité */
 %right RARROW
@@ -39,3 +39,4 @@ main_tactic:
 tactic:
   | INTRO VAR_NAME DOT                    { Intro $2 }
   | ASSUMPTION DOT                        { Assumption }
+  | APPLY VAR_NAME DOT                    { Apply $2 }
diff --git a/tactic.ml b/tactic.ml
index b5b76c9..2f9dbfb 100644
--- a/tactic.ml
+++ b/tactic.ml
@@ -2,4 +2,5 @@ open Structs;;
 
 type tactic =
   | Intro of var_lambda
-  | Assumption;;
+  | Assumption
+  | Apply of var_lambda;;