diff --git a/lexer.mll b/lexer.mll
index 21db775..61e9715 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -37,6 +37,8 @@ rule token = parse
   | "intro"         { INTRO }
   | "cut"           { CUT }
   | "apply"         { APPLY }
+  | "left"          { LEFT }
+  | "right"         { RIGHT }
 
   | var_id as s     { VARID(s) }
   | ty_id as s      { TYID(s) }
diff --git a/parser.mly b/parser.mly
index 3725d09..0fc0fab 100644
--- a/parser.mly
+++ b/parser.mly
@@ -9,19 +9,20 @@ open Parser_entry
 %token PLUS TIMES
 %token TOP BOT EXFALSO TILDE
 %token LPAREN RPAREN
-%token AND OR
 %token FUN ARR COLON TARR
+%token AND OR
 %token <string> VARID
 %token <string> TYID
 
 %token GOAL EXACT ASSUMPTION INTRO INTROS CUT APPLY
+%token LEFT RIGHT
 
 %token EOL
 
-%right TARR
-%right TILDE
 %right AND
 %right OR
+%right TARR
+%right TILDE
 
 %start main
 %type <parser_entry> main
@@ -41,6 +42,8 @@ command:
   | ASSUMPTION            { Tact (Assumption) }
   | INTROS                { Tact (Intros) }
   | INTRO                 { Tact (Intro) }
+  | RIGHT                 { Tact (Right) }
+  | LEFT                  { Tact (Left) }
   | CUT t=ty              { Tact (Cut t) }
   | APPLY s=TYID          { Tact (Apply s) }
 
diff --git a/proof.ml b/proof.ml
index 35185d3..c1e298e 100644
--- a/proof.ml
+++ b/proof.ml
@@ -23,6 +23,8 @@ type tactic =
   | Intro
   | Cut of ty
   | Apply of id
+  | Right
+  | Left
 
 let count = ref 0
 let get_fresh_hyp () =
@@ -168,6 +170,24 @@ let tact_intros : proof -> proof =
     with TacticFailed _ -> p
   in push
 
+let tact_right ((g, gs) : proof) : proof =
+  match g with
+  None -> raise (TacticFailed "no current goal")
+  | Some (h, goal_ty, cs) ->
+    match goal_ty with
+    | Or(_, t) ->
+      Some (h, t, cs), gs
+    | _ -> raise (TacticFailed "Not a disjunction")
+
+let tact_left ((g, gs) : proof) : proof =
+  match g with
+  None -> raise (TacticFailed "no current goal")
+  | Some (h, goal_ty, cs) ->
+    match goal_ty with
+    | Or(t, _) ->
+      Some (h, t, cs), gs
+    | _ -> raise (TacticFailed "Not a disjunction")
+
 let apply_tactic (p : proof) (t : tactic) : proof =
   match t with
   Exact_term e -> tact_exact_term p e
@@ -177,6 +197,8 @@ let apply_tactic (p : proof) (t : tactic) : proof =
   | Assumption -> tact_assumption p
   | Cut t -> tact_cut p t
   | Apply h -> tact_apply p h
+  | Right -> tact_right p
+  | Left -> tact_left p
 
 
 let tact_try (p : proof) (t : tactic) : proof =