diff --git a/lexer.mll b/lexer.mll
index 61e9715..1824b09 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -39,6 +39,7 @@ rule token = parse
   | "apply"         { APPLY }
   | "left"          { LEFT }
   | "right"         { RIGHT }
+  | "split"         { SPLIT }
 
   | var_id as s     { VARID(s) }
   | ty_id as s      { TYID(s) }
diff --git a/parser.mly b/parser.mly
index 0fc0fab..30e29bc 100644
--- a/parser.mly
+++ b/parser.mly
@@ -15,7 +15,7 @@ open Parser_entry
 %token <string> TYID
 
 %token GOAL EXACT ASSUMPTION INTRO INTROS CUT APPLY
-%token LEFT RIGHT
+%token LEFT RIGHT SPLIT
 
 %token EOL
 
@@ -42,6 +42,7 @@ command:
   | ASSUMPTION            { Tact (Assumption) }
   | INTROS                { Tact (Intros) }
   | INTRO                 { Tact (Intro) }
+  | SPLIT                 { Tact (Split) }
   | RIGHT                 { Tact (Right) }
   | LEFT                  { Tact (Left) }
   | CUT t=ty              { Tact (Cut t) }
diff --git a/proof.ml b/proof.ml
index c1e298e..d47215f 100644
--- a/proof.ml
+++ b/proof.ml
@@ -23,6 +23,7 @@ type tactic =
   | Intro
   | Cut of ty
   | Apply of id
+  | Split
   | Right
   | Left
 
@@ -170,6 +171,16 @@ let tact_intros : proof -> proof =
     with TacticFailed _ -> p
   in push
 
+let tact_split ((g, gs) : proof) : proof =
+  match g with
+  None -> raise (TacticFailed "no current goal")
+  | Some (h, goal_ty, cs) ->
+    match goal_ty with
+    | And(t1, t2) ->
+      Some (h, t1, cs), (h, t2, cs)::gs
+    | _ -> raise (TacticFailed "Not a conjonction")
+
+
 let tact_right ((g, gs) : proof) : proof =
   match g with
   None -> raise (TacticFailed "no current goal")
@@ -197,6 +208,7 @@ let apply_tactic (p : proof) (t : tactic) : proof =
   | Assumption -> tact_assumption p
   | Cut t -> tact_cut p t
   | Apply h -> tact_apply p h
+  | Split -> tact_split p
   | Right -> tact_right p
   | Left -> tact_left p