diff --git a/HOL.lp b/HOL.lp
index 8bb76f7..f5e4ac6 100644
--- a/HOL.lp
+++ b/HOL.lp
@@ -1,7 +1,15 @@
 require open Stdlib.Set;
 
-symbol ⤳ : Set → Set → Set; // \leadsto
+constant symbol ⤳ : Set → Set → Set; // \leadsto
 
 notation ⤳ infix right 20;
 
-rule τ ($x ⤳ $y) ↪ τ $x → τ $y;
+rule τ ($a ⤳ $b) ↪ τ $a → τ $b;
+
+injective symbol ⤳d : Π a:Set, (τ a → Set) → Set;
+
+notation ⤳d infix right 20;
+
+rule $a ⤳d λ _,$b.[] ↪ $a ⤳ $b;
+
+rule τ ($a ⤳d λ x,$b.[x]) ↪ Π x:τ $a, τ $b.[x];
diff --git a/Prop.lp b/Prop.lp
index 2bfa70c..32f0f22 100644
--- a/Prop.lp
+++ b/Prop.lp
@@ -8,7 +8,7 @@ builtin "Prop" ≔ Prop;
 
 injective symbol π : Prop → TYPE; // `p
 
-builtin "P" ≔ π;
+builtin "Prf" ≔ π;
 
 // true
 
diff --git a/Set.lp b/Set.lp
index fea919a..81d1758 100644
--- a/Set.lp
+++ b/Set.lp
@@ -10,7 +10,7 @@ constant symbol ι : Set;
 
 injective symbol τ : Set → TYPE; // `t or \tau
 
-builtin "T" ≔ τ;
+builtin "El" ≔ τ;
 
 // We assume that sets are non-empty
 
diff --git a/Tactic.lp b/Tactic.lp
index 6d4597e..2b37519 100644
--- a/Tactic.lp
+++ b/Tactic.lp
@@ -1,31 +1,47 @@
 // define a type representing Lambdapi tactics
 
-require open Stdlib.String Stdlib.Option Stdlib.List;
-
-constant symbol Tactic : TYPE;
+require open Stdlib.String Stdlib.Univ;
 
 // mandatory builtins
 
+constant symbol Tactic : TYPE;
+builtin "Tactic" ≔ Tactic;
+
 constant symbol #admit : Tactic;
 builtin "admit" ≔ #admit;
 
-symbol & : Tactic → Tactic → Tactic;
-builtin "and" ≔ &;
-notation & infix right 10;
+constant symbol #all_hyps: (Π [l] [a:U l], η a → Tactic) → Tactic;
+builtin "all_hyps" ≔ #all_hyps;
 
-constant symbol #apply [p] : π p → Tactic;
+constant symbol #apply: Π [l] [a:U l], η a → Tactic;
 builtin "apply" ≔ #apply;
 
-constant symbol #assume : String → Tactic;
+constant symbol #assume : String → Π [l], Π [a:U l], (η a → Tactic) → Tactic;
 builtin "assume" ≔ #assume;
 
+constant symbol #assumption : Tactic;
+builtin "assumption" ≔ #assumption;
+
+constant symbol #change: Π [l] [a:U l], η a → Tactic;
+builtin "change" ≔ #change;
+
+constant symbol & : Tactic → Tactic → Tactic;
+builtin "compose" ≔ &;
+notation & infix right 10;
+
 constant symbol #fail : Tactic;
 builtin "fail" ≔ #fail;
 
-constant symbol #generalize : Π [a], τ a → Tactic;
+constant symbol #first_hyp: (Π [l] [a:U l], η a → Tactic) → Tactic;
+builtin "first_hyp" ≔ #first_hyp;
+
+constant symbol #focus : String → Tactic;
+builtin "focus" ≔ #focus;
+
+constant symbol #generalize : Π [l] [a:U l], η a → Tactic;
 builtin "generalize" ≔ #generalize;
 
-constant symbol #have : String → Prop → Tactic;
+constant symbol #have : String → Π [l] [a:U l], η a → Tactic;
 builtin "have" ≔ #have;
 
 constant symbol #induction : Tactic;
@@ -34,22 +50,25 @@ builtin "induction" ≔ #induction;
 constant symbol #orelse : Tactic → Tactic → Tactic;
 builtin "orelse" ≔ #orelse;
 
-constant symbol #refine [p] : π p → Tactic;
+constant symbol #print : String → Tactic;
+builtin "print" ≔ #print;
+
+constant symbol #refine: String → Tactic;
 builtin "refine" ≔ #refine;
 
 constant symbol #reflexivity : Tactic;
 builtin "reflexivity" ≔ #reflexivity;
 
-constant symbol #remove : Π [a], π a → Tactic;
+constant symbol #remove : Π [l] [a:U l], η a → Tactic;
 builtin "remove" ≔ #remove;
 
 constant symbol #repeat : Tactic → Tactic;
 builtin "repeat" ≔ #repeat;
 
- symbol #rewrite : String → String → Π [a], π a → Tactic;
+ symbol #rewrite : String → String → Π [l] [a:U l], η a → Tactic;
 builtin "rewrite" ≔ #rewrite;
 
-constant symbol #set : String → Π [a], τ a → Tactic;
+constant symbol #set : String → Π [l] [a:U l], η a → Tactic;
 builtin "set" ≔ #set;
 
 constant symbol #simplify : Tactic;
@@ -70,9 +89,6 @@ builtin "try" ≔ #try;
 constant symbol #why3 : Tactic;
 builtin "why3" ≔ #why3;
 
-constant symbol #change : Tactic;
-builtin "change" ≔ #change;
-
 // defined tactics
 
 symbol nothing ≔ #try #fail;
diff --git a/Univ.lp b/Univ.lp
new file mode 100644
index 0000000..1b76885
--- /dev/null
+++ b/Univ.lp
@@ -0,0 +1,34 @@
+require open Stdlib.Set Stdlib.Prop;
+
+constant symbol L:TYPE;
+
+builtin "Level" ≔ L;
+
+constant symbol prop:L;
+constant symbol set_:L;
+
+injective symbol U:L → TYPE;
+
+builtin "Univ" ≔ U;
+
+rule U prop ↪ Prop
+with U set_ ↪ Set;
+
+injective symbol η:Π [l:L], U l → TYPE; // \eta
+
+builtin "Type" ≔ η;
+
+rule @η prop ↪ π
+with @η set_ ↪ τ;
+
+unif_rule @η $l $a ≡ π $b ↪ [$l ≡ prop; $a ≡ $b];
+unif_rule @η $l $a ≡ τ $b ↪ [$l ≡ set_; $a ≡ $b];
+
+require open Stdlib.FOL;
+
+unif_rule @η $l $a ≡ Π x:τ $b, π $c.[x] ↪ [$l ≡ prop; $a ≡ @∀ $b (λ x:τ $b, $c.[x])];
+
+require open Stdlib.HOL;
+
+unif_rule @η $l $a ≡ Π _:τ $b, τ $c.[] ↪ [$l ≡ set_; $a ≡ $b ⤳ $c.[]];
+unif_rule @η $l $a ≡ Π x:τ $b, τ $c.[x] ↪ [$l ≡ set_; $a ≡ $b ⤳d λ x:τ $b, $c.[x]];