diff --git a/lexer.mll b/lexer.mll
index f6f533a..57568b4 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -19,5 +19,6 @@ and token_tactic = parse
   | "intro"                     { INTRO }
   | "assumption"                { ASSUMPTION }
   | "apply"                     { APPLY }
+  | "elim"                      { ELIM }
   | ['a'-'z']+['0'-'9']* as s   { VAR_NAME s }
   | '.'                         { DOT }
diff --git a/main.ml b/main.ml
index 89f4fb1..3b4b933 100644
--- a/main.ml
+++ b/main.ml
@@ -132,6 +132,16 @@ while !subgoals <> [] do
             in
             explore hyps;
         )
+      | 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;
+        )
 done;
 
 let finalLam = !fill_holes [] in
diff --git a/parser.mly b/parser.mly
index 7d52621..d0745c9 100644
--- a/parser.mly
+++ b/parser.mly
@@ -10,7 +10,7 @@
 %token <string> VAR_NAME
 %token <string> TYPE_NAME
 
-%token DOT INTRO ASSUMPTION APPLY
+%token DOT INTRO ASSUMPTION APPLY ELIM
 
 /* L'ordre de définition définit la priorité */
 %right RARROW
@@ -40,3 +40,4 @@ tactic:
   | INTRO VAR_NAME DOT                    { Intro $2 }
   | ASSUMPTION DOT                        { Assumption }
   | APPLY VAR_NAME DOT                    { Apply $2 }
+  | ELIM VAR_NAME DOT                     { Elim $2 }
diff --git a/tactic.ml b/tactic.ml
index 2f9dbfb..a71071a 100644
--- a/tactic.ml
+++ b/tactic.ml
@@ -3,4 +3,5 @@ open Structs;;
 type tactic =
   | Intro of var_lambda
   | Assumption
-  | Apply of var_lambda;;
+  | Apply of var_lambda
+  | Elim of var_lambda;;