diff --git a/Option.lp b/Option.lp
new file mode 100644
index 0000000..fc6b590
--- /dev/null
+++ b/Option.lp
@@ -0,0 +1,8 @@
+// option type
+
+require open Stdlib.Set;
+
+constant symbol option : Set → Set;
+
+constant symbol none [a] : τ (option a);
+constant symbol some [a] : τ a → τ (option a);
diff --git a/String.lp b/String.lp
new file mode 100644
index 0000000..d96fbc7
--- /dev/null
+++ b/String.lp
@@ -0,0 +1,12 @@
+// builtin type of strings
+
+require open Stdlib.Set;
+
+constant symbol String : TYPE;
+builtin "String" ≔ String;
+
+constant symbol string : Set;
+rule τ string ↪ String;
+
+constant symbol gen_id : String → String;
+builtin "gen_id" ≔ gen_id;
diff --git a/Tactic.lp b/Tactic.lp
new file mode 100644
index 0000000..37b8aaf
--- /dev/null
+++ b/Tactic.lp
@@ -0,0 +1,89 @@
+// define a type representing Lambdapi tactics
+
+require open Stdlib.Set Stdlib.Prop Stdlib.String Stdlib.Option
+             Stdlib.List;
+
+constant symbol Tactic : TYPE;
+
+constant symbol #admit : Tactic;
+builtin "admit" ≔ #admit;
+
+symbol & : Tactic → Tactic → Tactic;
+builtin "and" ≔ &;
+notation & infix right 10;
+
+constant symbol #apply [p] : π p → Tactic;
+builtin "apply" ≔ #apply;
+
+constant symbol #assume : τ (list string) → Tactic;
+builtin "assume" ≔ #assume;
+
+constant symbol #fail : Tactic;
+builtin "fail" ≔ #fail;
+
+//constant symbol #generalize : Π [a], τ a → Tactic;
+//builtin "generalize" ≔ #generalize;
+
+constant symbol #have : String → Π p, π p → Tactic;
+builtin "have" ≔ #have;
+
+constant symbol #induction : Tactic;
+builtin "induction" ≔ #induction;
+
+constant symbol #orelse : Tactic → Tactic → Tactic;
+builtin "orelse" ≔ #orelse;
+
+constant symbol #refine [p] : π p → Tactic;
+builtin "refine" ≔ #refine;
+
+constant symbol #reflexivity : Tactic;
+builtin "reflexivity" ≔ #reflexivity;
+
+//constant symbol #remove : Π [a], π a → Tactic;
+//builtin "remove" ≔ #remove;
+
+constant symbol #repeat : Tactic → Tactic;
+builtin "repeat" ≔ #repeat;
+
+constant symbol #rewrite [p] : π p → Tactic;
+builtin "rewrite" ≔ #rewrite;
+
+constant symbol #set : String → Π [a], τ a → Tactic;
+builtin "set" ≔ #set;
+
+constant symbol #simplify : /* Π [a], τ a → */ Tactic;
+builtin "simplify" ≔ #simplify;
+
+constant symbol #solve : Tactic;
+builtin "solve" ≔ #solve;
+
+constant symbol #symmetry : Tactic;
+builtin "symmetry" ≔ #symmetry;
+
+constant symbol #try : Tactic → Tactic;
+builtin "try" ≔ #try;
+
+constant symbol #why3 : /*τ (option string) →*/ Tactic;
+builtin "why3" ≔ #why3;
+
+/*****************************************************************************/
+
+symbol nothing ≔ #repeat #fail;
+
+require open Stdlib.Nat;
+
+symbol * : ℕ → Tactic → Tactic;
+notation * infix 20;
+
+rule 0 * _ ↪ nothing
+with $n +1 * $t ↪ $t & ($n * $t);
+
+require open Stdlib.Eq;
+
+symbol lemma x y z t : π (((x + y) + z) + t = x + (y + (z + t))) ≔
+begin
+  assume x y z t;
+  //rewrite addnA; rewrite addnA; reflexivity
+  compute 2 * #rewrite addnA;
+  eval 2 * #rewrite addnA & #reflexivity
+end;