diff --git a/.github/workflows/type_check.yml b/.github/workflows/type_check.yml
index d965629a1ef3107e82c91e30b3c78d37eb1ede78..eee39ccb4346b1c71accb970c63af981018d27d4 100644
--- a/.github/workflows/type_check.yml
+++ b/.github/workflows/type_check.yml
@@ -30,7 +30,7 @@ jobs:
         sudo chmod 755 /usr/bin/opam
         opam init -a --disable-sandboxing --compiler="4.07.1"
         opam update
-        opam switch "4.07.1"
+        opam switch "4.11.1"
         eval $(opam env)
         opam install alt-ergo.2.3.0 --yes
         git clone https://github.com/Deducteam/lambdapi.git lambdapi
@@ -46,12 +46,12 @@ jobs:
         eval $(opam env)
         lambdapi check encodings/*.lp
 
-    - name: check paper
-      run: |
-        eval $(opam env)
-        lambdapi check paper/*.lp
+    # - name: check paper
+    #   run: |
+    #     eval $(opam env)
+    #     lambdapi check paper/*.lp
 
-    - name: check prelude
-      run: |
-        eval $(opam env)
-        lambdapi check prelude/*.lp
+    # - name: check prelude
+    #   run: |
+    #     eval $(opam env)
+    #     lambdapi check prelude/*.lp
diff --git a/encodings/bool_plus.lp b/encodings/bool_plus.lp
index c5683c42b88735e8d74a9cf5a6df0af1d9783531..e357e7cff162d0a7a60b56fce7dcf22a392e4f50 100644
--- a/encodings/bool_plus.lp
+++ b/encodings/bool_plus.lp
@@ -1,20 +1,20 @@
 require open personoj.encodings.lhol
-require open personoj.encodings.prenex
-require open personoj.encodings.logical
+             personoj.encodings.prenex
+             personoj.encodings.logical;
 
 // It may be generalisable to dependent propositions
 opaque
 symbol and_intro:
   Prf
-  (∀ {prop} (λa,
-   ∀ {prop} (λb,
-   a ⊃ (λ_, b ⊃ (λ_, a ∧ (λ_, b)))))) ≔
+  (∀ {prop} (λ a,
+   ∀ {prop} (λ b,
+   a ⊃ (λ _, b ⊃ (λ _, a ∧ (λ _, b)))))) ≔
 begin
-  assume A B h0 h1 f
-  refine f h0 h1
-end
+  assume A B h0 h1 f;
+  refine f h0 h1;
+end;
 
 opaque
-symbol and_elim_1 a b (_: Prf (a ∧ (λ_, b))): Prf a ≔
+symbol and_elim_1 a b (_: Prf (a ∧ (λ _, b))): Prf a ≔
 begin
-admit
+admit;
diff --git a/encodings/builtins.lp b/encodings/builtins.lp
index e07523314c8c2fa707303242d2c7dbcd15bf8088..f45b729dd67aed375260798de9df0a24a5d0b314 100644
--- a/encodings/builtins.lp
+++ b/encodings/builtins.lp
@@ -1,34 +1,33 @@
 require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.logical
-require open personoj.encodings.equality
-require open personoj.encodings.prenex
+             personoj.encodings.pvs_cert
+             personoj.encodings.logical
+             personoj.encodings.equality
+             personoj.encodings.prenex;
 
-constant symbol {|!Number!|}: Set
+constant symbol {|!Number!|}: Set;
 
-constant symbol zero: El {|!Number!|}
-constant symbol succ: El ({|!Number!|} ~> {|!Number!|})
+constant symbol zero: El {|!Number!|};
+constant symbol succ: El ({|!Number!|} ~> {|!Number!|});
 
-set builtin "0" ≔ zero
-set builtin "+1" ≔ succ
+set builtin "0" ≔ zero;
+set builtin "+1" ≔ succ;
 
 // In PVS, the axipms 1 ≠ 2, 1≠3, ... are built in
 // Here we use the decidable equality
 rule Prf (succ $n = succ $m) ↪ Prf ($n = $m)
 with Prf (zero = succ _) ↪ Prf false
-with Prf (zero = zero) ↪ Prf true
+with Prf (zero = zero) ↪ Prf true;
 
 // Define strings as list of numbers
-constant symbol {|!String!|}: Set
-constant symbol str_empty: El {|!String!|}
-constant symbol str_cons: El {|!Number!|} → El {|!String!|} → El {|!String!|}
+constant symbol {|!String!|}: Set;
+constant symbol str_empty: El {|!String!|};
+constant symbol str_cons: El {|!Number!|} → El {|!String!|} → El {|!String!|};
 
-set declared "∃"
-symbol ∃ {T: Set} (P: El T → El prop) ≔ ¬ (∀ (λx, ¬ (P x)))
+symbol ∃ {T: Set} (P: El T → El prop) ≔ ¬ (∀ (λ x, ¬ (P x)));
 
 symbol propositional_extensionality:
-  Prf (∀ {prop} (λp, (∀ {prop} (λq, (iff p q) ⊃ (λ_, eq {prop} p q)))))
+  Prf (∀ {prop} (λ p, (∀ {prop} (λ q, (iff p q) ⊃ (λ _, eq {prop} p q)))));
 
-symbol neq {t} x y ≔ ¬ (eq {t} x y)
-set infix left 2 "/=" ≔ neq
-set infix left 2 "≠" ≔ neq
+symbol neq {t} x y ≔ ¬ (eq {t} x y);
+set infix left 2 "/=" ≔ neq;
+set infix left 2 "≠" ≔ neq;
diff --git a/encodings/deptype.lp b/encodings/deptype.lp
index ffc1bff0e3794aef628e7372f3d022015f3633e2..3b0c5176d272ad83f32ecfdbf48a8cf4df4b9be6 100644
--- a/encodings/deptype.lp
+++ b/encodings/deptype.lp
@@ -6,9 +6,9 @@
 /// cons(n: nat, r: real, v: vector_real[n].vec): vector_real[n + 1].vec
 
 require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.prenex
+             personoj.encodings.pvs_cert
+             personoj.encodings.prenex;
 
-constant symbol darr: Set → Kind → Kind
-set infix right 6 "*>" ≔ darr
-rule Ty ($t *> $k) ↪ El $t → Ty $k
+constant symbol darr: Set → Kind → Kind;
+set infix right 6 "*>" ≔ darr;
+rule Ty ($t *> $k) ↪ El $t → Ty $k;
diff --git a/encodings/equality.lp b/encodings/equality.lp
index 5d0e7040cf3e843eb2d95ddd89c399d42a0cbb86..6d71cede60f247a275b96649f85aebed7182ac2f 100644
--- a/encodings/equality.lp
+++ b/encodings/equality.lp
@@ -2,34 +2,34 @@
 require open
   personoj.encodings.lhol
   personoj.encodings.pvs_cert
-  personoj.encodings.logical
+  personoj.encodings.logical;
 
 // We don't use prenex encoding to have implicit arguments.
-symbol eq {s: Set}: El s → El s → Prop
-set infix left 2 "=" ≔ eq
-set builtin "eq" ≔ eq
+symbol eq {s: Set}: El s → El s → Prop;
+set infix left 2 "=" ≔ eq;
+set builtin "eq" ≔ eq;
 
-rule @eq (@psub $t $p) $x $y ↪ @eq $t (@fst $t $p $x) (@fst $t $p $y)
+rule @eq (@psub $t $p) $x $y ↪ @eq $t (@fst $t $p $x) (@fst $t $p $y);
 
-symbol neq {s: Set} (x y: El s) ≔ ¬ (x = y)
-set infix 2 "≠" ≔ neq
+symbol neq {s: Set} (x y: El s) ≔ ¬ (x = y);
+set infix 2 "≠" ≔ neq;
 
 // Leibniz equality
-rule Prf ($x = $y) ↪ Πp: El (_ ~> prop), Prf (p $x) → Prf (p $y)
+rule Prf ($x = $y) ↪ Π p: El (_ ~> prop), Prf (p $x) → Prf (p $y);
 
 // Some theorems for equality
 opaque
 symbol eq_refl {a: Set} (x: El a): Prf (x = x) ≔
 begin
-  assume a x p h
-  apply h
-end
-set builtin "refl" ≔ eq_refl
+  assume a x p h;
+  apply h;
+end;
+set builtin "refl" ≔ eq_refl;
 
 opaque
 symbol eq_trans {a: Set} (x y z: El a) (_: Prf (x = y)) (_: Prf (y = z))
       : Prf (x = z) ≔
 begin
-  assume a x y z hxy hyz p px
-  refine hyz p (hxy p px)
-end
+  assume a x y z hxy hyz p px;
+  refine hyz p (hxy p px);
+end;
diff --git a/encodings/equality_tup.lp b/encodings/equality_tup.lp
index 555e677188ca5d513cafac9cf72e2a1c6b01dacd..e4a9b3cc181bcbcbadd1608a9d16baa75811f0db 100644
--- a/encodings/equality_tup.lp
+++ b/encodings/equality_tup.lp
@@ -1,12 +1,12 @@
 // Equality defined on tuple of arguments
 require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require personoj.encodings.tuple as T
-require open personoj.encodings.logical
+             personoj.encodings.pvs_cert;
+require personoj.encodings.tuple as T;
+require open personoj.encodings.logical;
 
 // Equality operates on the maximal supertype. It allows to profit
 // from predicate subtyping for free in the propositional equality.
-symbol eq {t: Set} (_: El (T.t t t)): Prop
-symbol neq {t} m ≔ ¬ (@eq t m)
+symbol eq {t: Set} (_: El (T.t t t)): Prop;
+symbol neq {t} m ≔ ¬ (@eq t m);
 rule @eq (@psub $t $p) (T.cons $x $y)
-   ↪ @eq $t (T.cons (@fst $t $p $x) (@fst $t $p $y))
+   ↪ @eq $t (T.cons (@fst $t $p $x) (@fst $t $p $y));
diff --git a/encodings/if.lp b/encodings/if.lp
index 17b5d62bb7e75ffe1bad4b9e687a1b408052e8c9..9248a1158bb314c84f3ad2ccaf9d093df77d71ca 100644
--- a/encodings/if.lp
+++ b/encodings/if.lp
@@ -1,31 +1,31 @@
 // Close to PVS logic system: native equality,
 // true, false, and if
 require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
+             personoj.encodings.pvs_cert;
 
-symbol false ≔ ∀ {prop} (λx, x)
-symbol true ≔ impd {false} (λ_, false)
+symbol false ≔ ∀ {prop} (λ x, x);
+symbol true ≔ impd {false} (λ _, false);
 
-symbol eq {s: Set}: El s → El s → El prop
-set infix left 6 "=" ≔ eq
+symbol eq {s: Set}: El s → El s → El prop;
+set infix left 6 "=" ≔ eq;
 
-symbol not p ≔ eq {prop} p false
-set prefix 5 "¬" ≔ not
+symbol not p ≔ eq {prop} p false;
+set prefix 5 "¬" ≔ not;
 
-constant symbol if {s: Set} p: (Prf p → El s) → (Prf (¬ p) → El s) → El s
+constant symbol if {s: Set} p: (Prf p → El s) → (Prf (¬ p) → El s) → El s;
 rule Prf (if $p $then $else)
-   ↪ (Πh: Prf $p, Prf ($then h)) → Πh: Prf (¬ $p), Prf ($else h)
+   ↪ (Π h: Prf $p, Prf ($then h)) → Π h: Prf (¬ $p), Prf ($else h);
 
-symbol and p q ≔ if {prop} p q (λ_, false)
-symbol or p q ≔ if {prop} p (λ_, true) q
-symbol imp p q ≔ if {prop} p q (λ_, true)
-set infix left 4 "∧" ≔ and
-set infix left 3 "∨" ≔ or
-set infix left 2 "⊃" ≔ imp
+symbol and p q ≔ if {prop} p q (λ _, false);
+symbol or p q ≔ if {prop} p (λ _, true) q;
+symbol imp p q ≔ if {prop} p q (λ _, true);
+set infix left 4 "∧" ≔ and;
+set infix left 3 "∨" ≔ or;
+set infix left 2 "⊃" ≔ imp;
 
-set builtin "bot" ≔ false
-set builtin "top" ≔ true
-set builtin "not" ≔ not
-set builtin "imp" ≔ imp
-set builtin "and" ≔ and
-set builtin "or"  ≔ or
+set builtin "bot" ≔ false;
+set builtin "top" ≔ true;
+set builtin "not" ≔ not;
+set builtin "imp" ≔ imp;
+set builtin "and" ≔ and;
+set builtin "or"  ≔ or;
diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 11a2e30d52b931c0969ff38c99b29b9052e52f33..67db8c4a5655b0c2634c75407b6890d856e4877d 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -1,28 +1,27 @@
 /// Encoding of λHOL
-symbol Kind: TYPE
-symbol Set: TYPE
-symbol Prop: TYPE
+symbol Kind: TYPE;
+symbol Set: TYPE;
+symbol Prop: TYPE;
 
-set declared "∀"
-injective symbol El: Set → TYPE
-injective symbol Prf: Prop → TYPE
+injective symbol El: Set → TYPE;
+injective symbol Prf: Prop → TYPE;
 
-constant symbol {|set|}: Kind
-constant symbol prop: Set
+constant symbol {|set|}: Kind;
+constant symbol prop: Set;
 
-rule El prop ↪ Prop
+rule El prop ↪ Prop;
 
-constant symbol ∀ {x: Set}: (El x → Prop) → Prop
-constant symbol impd {x: Prop}: (Prf x → Prop) → Prop
-constant symbol arrd {x: Set}: (El x → Set) → Set
+constant symbol ∀ {x: Set}: (El x → Prop) → Prop;
+constant symbol impd {x: Prop}: (Prf x → Prop) → Prop;
+constant symbol arrd {x: Set}: (El x → Set) → Set;
 
-rule Prf (∀ {$X} $P) ↪ Πx: El $X, Prf ($P x)
-with Prf (impd {$H} $P) ↪ Πh: Prf $H, Prf ($P h)
-with El (arrd {$X} $T) ↪ Πx: El $X, El ($T x)
+rule Prf (∀ {$X} $P) ↪ Π x: El $X, Prf ($P x)
+with Prf (impd {$H} $P) ↪ Π h: Prf $H, Prf ($P h)
+with El (arrd {$X} $T) ↪ Π x: El $X, El ($T x);
 
-constant symbol arr: Set → Set → Set
-rule El (arr $X $Y) ↪ (El $X) → (El $Y)
-set infix right 6 "~>" ≔ arr
+constant symbol arr: Set → Set → Set;
+rule El (arr $X $Y) ↪ (El $X) → (El $Y);
+set infix right 6 "~>" ≔ arr;
 
-set builtin "T" ≔ El
-set builtin "P" ≔ Prf
+set builtin "T" ≔ El;
+set builtin "P" ≔ Prf;
diff --git a/encodings/logical.lp b/encodings/logical.lp
index 521204c1dbf09aa58b8b6655f3d83137605c09fb..33139097f6c1bf9e1902622d127d1a8acd3e9321 100644
--- a/encodings/logical.lp
+++ b/encodings/logical.lp
@@ -1,28 +1,28 @@
 // Definition based on implication
-require open personoj.encodings.lhol
+require open personoj.encodings.lhol;
 
-symbol false ≔ ∀ {prop} (λx, x)
-symbol true ≔ impd {false} (λ_, false)
+symbol false ≔ ∀ {prop} (λ x, x);
+symbol true ≔ impd {false} (λ _, false);
 
-symbol not P ≔ impd {P} (λ_, false)
-set prefix 5 "¬" ≔ not
+symbol not P ≔ impd {P} (λ _, false);
+set prefix 5 "¬" ≔ not;
 
-symbol imp P Q ≔ impd {P} Q
-set infix 2 "⊃" ≔ imp
+symbol imp P Q ≔ impd {P} Q;
+set infix 2 "⊃" ≔ imp;
 
-symbol and P Q ≔ ¬ (P ⊃ (λh, ¬ (Q h)))
-set infix 4 "∧" ≔ and
-symbol or P Q ≔ (¬ P) ⊃ Q
-set infix 3 "∨" ≔ or
+symbol and P Q ≔ ¬ (P ⊃ (λ h, ¬ (Q h)));
+set infix 4 "∧" ≔ and;
+symbol or P Q ≔ (¬ P) ⊃ Q;
+set infix 3 "∨" ≔ or;
 
-set builtin "bot" ≔ false
-set builtin "top" ≔ true
-set builtin "not" ≔ not
-set builtin "imp" ≔ imp
-set builtin "and" ≔ and
-set builtin "or"  ≔ or
+set builtin "bot" ≔ false;
+set builtin "top" ≔ true;
+set builtin "not" ≔ not;
+set builtin "imp" ≔ imp;
+set builtin "and" ≔ and;
+set builtin "or"  ≔ or;
 
-symbol if {s: Set} (p: Prop): (Prf p → El s) → (Prf (¬ p) → El s) → El s
-rule if {prop} $p $then $else ↪ ($p ⊃ $then) ⊃ (λ_, (¬ $p) ⊃ $else)
+symbol if {s: Set} (p: Prop): (Prf p → El s) → (Prf (¬ p) → El s) → El s;
+rule if {prop} $p $then $else ↪ ($p ⊃ $then) ⊃ (λ _, (¬ $p) ⊃ $else);
 
-symbol iff P Q ≔ (P ⊃ (λ_, Q)) ∧ ((λ_, Q ⊃ (λ_, P)))
+symbol iff P Q ≔ (P ⊃ (λ _, Q)) ∧ ((λ _, Q ⊃ (λ _, P)));
diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index 2b96a639868a80a957c8ffd845860905a183d798..85023a753feff74bcf5b7ea12a1022659eae6bdc 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -5,34 +5,30 @@
 /// groups[t: TYPE]: THEORY BEGIN ... END groups
 /// For more informations on the encoding of prenex polymorphism, see
 /// https://arxiv.org/abs/1807.01873 and theory U
-require open personoj.encodings.lhol
-
-// Quantification for objects of type ‘Kind’
-set declared "∀K"
-// Quantification for objects of type ‘Set’
-set declared "∀S"
-// Quantification for objects of type ‘Prop’
-set declared "∀B"
+require open personoj.encodings.lhol;
 
 // To interpret PVS sorts
-injective symbol Ty : Kind → TYPE
-rule Ty {|set|} ↪ Set
+injective symbol Ty : Kind → TYPE;
+rule Ty {|set|} ↪ Set;
 
-constant symbol SchemeK: TYPE
-injective symbol El_k: SchemeK → TYPE
-constant symbol scheme_k: Kind → SchemeK
-rule El_k (scheme_k $X) ↪ Ty $X
+// Quantification for objects of type ‘Kind’
+constant symbol SchemeK: TYPE;
+injective symbol El_k: SchemeK → TYPE;
+constant symbol scheme_k: Kind → SchemeK;
+rule El_k (scheme_k $X) ↪ Ty $X;
 
-constant symbol ∀K: (Set → SchemeK) → SchemeK
-rule El_k (∀K $e) ↪ Πt: Set, El_k ($e t)
+constant symbol ∀K: (Set → SchemeK) → SchemeK;
+rule El_k (∀K $e) ↪ Π t: Set, El_k ($e t);
 
-constant symbol SchemeS: TYPE
-injective symbol El_s: SchemeS → TYPE
-constant symbol scheme_s: Set → SchemeS
-rule El_s (scheme_s $X) ↪ El $X
+// Quantification for objects of type ‘Set’
+constant symbol SchemeS: TYPE;
+injective symbol El_s: SchemeS → TYPE;
+constant symbol scheme_s: Set → SchemeS;
+rule El_s (scheme_s $X) ↪ El $X;
 
-constant symbol ∀S: (Set → SchemeS) → SchemeS
-rule El_s (∀S $e) ↪ Πt: Set, El_s ($e t)
+constant symbol ∀S: (Set → SchemeS) → SchemeS;
+rule El_s (∀S $e) ↪ Π t: Set, El_s ($e t);
 
-constant symbol ∀B: (Set → Prop) → Prop
-rule Prf (∀B $p) ↪ Πx: Set, Prf ($p x)
+// Quantification for objects of type ‘Prop’
+constant symbol ∀B: (Set → Prop) → Prop;
+rule Prf (∀B $p) ↪ Π x: Set, Prf ($p x);
diff --git a/encodings/pvs_cert.lp b/encodings/pvs_cert.lp
index 21ab64e9ed10b2e3b19bf8b162e73f457dd93c04..32918bf57ed256eb6630fd0fcbac47d994a836bc 100644
--- a/encodings/pvs_cert.lp
+++ b/encodings/pvs_cert.lp
@@ -1,16 +1,14 @@
 // PVS-Cert
-require open personoj.encodings.lhol
+require open personoj.encodings.lhol;
 
-set declared "μ"
+constant symbol psub {x: Set}: (El x → Prop) → Set;
+protected symbol pair': Π(t: Set) (p: El t → Prop), El t → El (psub p);
+symbol fst: Π{t: Set} {p: El t → Prop}, El (psub p) → El t;
 
-constant symbol psub {x: Set}: (El x → Prop) → Set
-protected symbol pair': Π(t: Set) (p: El t → Prop), El t → El (psub p)
-symbol fst: Π{t: Set} {p: El t → Prop}, El (psub p) → El t
-
-symbol snd {t: Set}{p: El t → Prop} (m: El (psub p)): Prf (p (fst m))
+symbol snd {t: Set} {p: El t → Prop} (m: El (psub p)): Prf (p (fst m));
 
 // Proof irrelevance
 symbol pair {t: Set} {p: El t → Prop} (m: El t) (_: Prf (p m))
-     ≔ pair' t p m
+     ≔ pair' t p m;
 
-rule fst (pair' _ _ $M) ↪ $M
+rule fst (pair' _ _ $M) ↪ $M;
diff --git a/encodings/pvs_cert_minus.lp b/encodings/pvs_cert_minus.lp
index d63c35f0db75fc7542e3ed38bed3048ee267b631..d796df4a32fe90c55edc1a06e6aa4aea1816aeb1 100644
--- a/encodings/pvs_cert_minus.lp
+++ b/encodings/pvs_cert_minus.lp
@@ -1,13 +1,12 @@
 // PVS-Cert-, or ECC with only one universe
-require open personoj.encodings.lhol
+require open personoj.encodings.lhol;
 
-set declared "Σ"
-constant symbol Σ (T : Set): (El T → Set) → Set
+constant symbol Σ (T : Set): (El T → Set) → Set;
 constant symbol pair {T: Set} {U: El T → Set} (M: El T) (_: El (U M))
-              : El (Σ T U)
+              : El (Σ T U);
 
-symbol fst {T: Set} {U: El T → Set}: El (Σ T U) → El T
-rule fst (pair $M _) ↪ $M
+symbol fst {T: Set} {U: El T → Set}: El (Σ T U) → El T;
+rule fst (pair $M _) ↪ $M;
 
-symbol snd {T: Set} {U: El T → Set} (M: El (Σ T U)): El (U (fst M))
-rule snd (pair _ $N) ↪ $N
+symbol snd {T: Set} {U: El T → Set} (M: El (Σ T U)): El (U (fst M));
+rule snd (pair _ $N) ↪ $N;
diff --git a/encodings/pvs_core.lp b/encodings/pvs_core.lp
index eee89932a36a56209f7eda6e74ef02148a1aefee..33fe4387a5c3950ac43a858e0f48c32cc1d6a820 100644
--- a/encodings/pvs_core.lp
+++ b/encodings/pvs_core.lp
@@ -1,39 +1,39 @@
-constant symbol Type : TYPE
-constant symbol Prop : Type
+constant symbol Type : TYPE;
+constant symbol Prop : Type;
 
-injective symbol El : Type → TYPE
-injective symbol Prf : El Prop → TYPE
+injective symbol El : Type → TYPE;
+injective symbol Prf : El Prop → TYPE;
 
-symbol arr : Type → Type → Type
-set infix right 6 "~>" ≔ arr
+symbol arr : Type → Type → Type;
+set infix right 6 "~>" ≔ arr;
 
-rule El ($A ~> $B) ↪ El $A → El $B
+rule El ($A ~> $B) ↪ El $A → El $B;
 
 // symbol psub : Π A : Type, El (A ~> Prop) → Type
-symbol psub : Π A : Type, (El A → El Prop) → Type
+symbol psub : Π A : Type, (El A → El Prop) → Type;
 
-constant symbol cast : Type → Type
-rule El (cast (psub $A _)) ↪ El $A
+constant symbol cast : Type → Type;
+rule El (cast (psub $A _)) ↪ El $A;
 
 symbol psubElim1 (A : Type) (P : El (A ~> Prop)):
-  El (psub A P) → El A
+  El (psub A P) → El A;
 
-symbol imp : El (Prop ~> Prop ~> Prop)
-set infix right 6 "I>" ≔ imp
+symbol imp : El (Prop ~> Prop ~> Prop);
+set infix right 6 "I>" ≔ imp;
 
-symbol impIntro : Π (p q : El Prop), (Prf p → Prf q) → Prf (p I> q)
-symbol impElim : Π p q : El Prop, Prf (p I> q) → Prf p → Prf q
+symbol impIntro : Π (p q : El Prop), (Prf p → Prf q) → Prf (p I> q);
+symbol impElim : Π (p q : El Prop), Prf (p I> q) → Prf p → Prf q;
 
-symbol all (A : Type): El (A ~> Prop) → El Prop
-rule El (all $A $P) ↪ Π x : El $A, El ($P x)
+symbol all (A : Type): El (A ~> Prop) → El Prop;
+rule El (all $A $P) ↪ Π x : El $A, El ($P x);
 
 // Forall intro
 symbol allIntro (A: Type) (p: El (A ~> Prop)) (x: El A):
-  Prf (p x) → Prf (all A p)
+  Prf (p x) → Prf (all A p);
 // Forall elim
 symbol allElim (A: Type) (t: El A) (p: El (A ~> Prop)):
-  Prf (all A p) → Prf (p t)
+  Prf (all A p) → Prf (p t);
 
 // Subtype elim 2
 symbol psubElim (A: Type) (p: El (A ~> Prop)) (t: El (cast (psub A p))):
-  Prf (p t)
+  Prf (p t);
diff --git a/encodings/sum.lp b/encodings/sum.lp
index a0b9357c75ee9a6bcbd5624bb9ed13a82a678585..82f13ac1878aaa181b02a21a70b0cce4e9cad504 100644
--- a/encodings/sum.lp
+++ b/encodings/sum.lp
@@ -1,9 +1,9 @@
 // Dependent sum type
-require open personoj.encodings.lhol
+require open personoj.encodings.lhol;
 
-constant symbol t (a: Set): (El a → Set) → Set
-symbol cons {a: Set} {b: El a → Set} (m: El a): El (b m) → El (t a b)
-symbol car {a: Set} {b: El a → Set}: El (t a b) → El a
-symbol cdr {a: Set} {b: El a → Set} (m: El (t a b)): El (b (car m))
-rule car (cons $m _) ↪ $m
-rule cdr (cons _ $n) ↪ $n
+constant symbol t (a: Set): (El a → Set) → Set;
+symbol cons {a: Set} {b: El a → Set} (m: El a): El (b m) → El (t a b);
+symbol car {a: Set} {b: El a → Set}: El (t a b) → El a;
+symbol cdr {a: Set} {b: El a → Set} (m: El (t a b)): El (b (car m));
+rule car (cons $m _) ↪ $m;
+rule cdr (cons _ $n) ↪ $n;
diff --git a/encodings/tuple.lp b/encodings/tuple.lp
index 708980026cb17adafd487d0c73be7ba0491510e6..ac98e504a81cf4c15bf8050448ae2295a3fd52e3 100644
--- a/encodings/tuple.lp
+++ b/encodings/tuple.lp
@@ -1,9 +1,9 @@
 // Non dependent tuples
-require open personoj.encodings.lhol
+require open personoj.encodings.lhol;
 
-constant symbol t: Set → Set → Set
-symbol cons {a: Set} {b: Set}: El a → El b → El (t a b)
-symbol car {a: Set} {b: Set}: El (t a b) → El a
-symbol cdr {a: Set} {b: Set}: El (t a b) → El b
-rule car (cons $x _) ↪ $x
-rule cdr (cons _ $y) ↪ $y
+constant symbol t: Set → Set → Set;
+symbol cons {a: Set} {b: Set}: El a → El b → El (t a b);
+symbol car {a: Set} {b: Set}: El (t a b) → El a;
+symbol cdr {a: Set} {b: Set}: El (t a b) → El b;
+rule car (cons $x _) ↪ $x;
+rule cdr (cons _ $y) ↪ $y;
diff --git a/encodings/unif_rules.lp b/encodings/unif_rules.lp
index ba75150680d33d0b2e75b052e1ffbfc21cc3095f..7d9925812439aa8a15c07082e55a306509ba60b5 100644
--- a/encodings/unif_rules.lp
+++ b/encodings/unif_rules.lp
@@ -1,3 +1,3 @@
-require open personoj.encodings.lhol
+require open personoj.encodings.lhol;
 
-set unif_rule El $t ≡ Prop ↪ $t ≡ prop
+set unif_rule El $t ≡ Prop ↪ [$t ≡ prop];
diff --git a/paper/proof_irr.lp b/paper/proof_irr.lp
index dd5e63cf2a78d4113feb0272a82d23f81087633c..02707e9a9cc02f862ae6a7271a47a6c76c23e3c8 100644
--- a/paper/proof_irr.lp
+++ b/paper/proof_irr.lp
@@ -1,57 +1,54 @@
 require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.logical
-require open personoj.encodings.equality
+             personoj.encodings.pvs_cert
+             personoj.encodings.logical
+             personoj.encodings.equality;
 
 
-set declared "â„•"
-constant symbol â„•: Set
-constant symbol z: El â„•
-constant symbol s (_: El â„•): El â„•
-constant symbol leq: El ℕ → El ℕ → Prop
-set infix left 3 "≤" ≔ leq
+constant symbol â„•: Set;
+constant symbol z: El â„•;
+constant symbol s (_: El â„•): El â„•;
+constant symbol leq: El ℕ → El ℕ → Prop;
+set infix left 3 "≤" ≔ leq;
 
 // Agda manual
-symbol p1: Prf (z ≤ s z)
-symbol p2: Prf (z ≤ s z)
-symbol bounded (k: El ℕ) ≔ psub (λn, n ≤ k)
+symbol p1: Prf (z ≤ s z);
+symbol p2: Prf (z ≤ s z);
+symbol bounded (k: El ℕ) ≔ psub (λ n, n ≤ k);
 
-constant symbol slist (_: El â„•): Set
-constant symbol snil (bound: El â„•): El (slist bound)
+constant symbol slist (_: El â„•): Set;
+constant symbol snil (bound: El â„•): El (slist bound);
 constant symbol scons {bound: El â„•} (head: El (bounded bound))
                       (_: El (slist (fst head)))
-              : El (slist bound)
+              : El (slist bound);
 
-set declared "l₁"
-set declared "lâ‚‚"
-symbol l₁: El (slist (s z)) ≔ scons (pair z p1) (snil z)
-symbol l₂: El (slist (s z)) ≔ scons (pair z p2) (snil z)
+symbol l₁: El (slist (s z)) ≔ scons (pair z p1) (snil z);
+symbol l₂: El (slist (s z)) ≔ scons (pair z p2) (snil z);
 
-opaque symbol listeq: Prf (l₁ = l₂) ≔ eq_refl l₁
+opaque symbol listeq: Prf (l₁ = l₂) ≔ eq_refl l₁;
 // begin
 //   refine eq_refl l₁
 // end
 
-constant symbol even_p: El ℕ → Prop
-symbol even ≔ psub even_p
+constant symbol even_p: El ℕ → Prop;
+symbol even ≔ psub even_p;
 
 // Proof irrelevance without K
-symbol eqEven (e1 e2: El even) ≔ fst e1 = fst e2
+symbol eqEven (e1 e2: El even) ≔ fst e1 = fst e2;
 
-symbol plus: El ℕ → El ℕ → El ℕ
-set infix left 10 "+" ≔ plus
+symbol plus: El ℕ → El ℕ → El ℕ;
+set infix left 10 "+" ≔ plus;
 
-symbol plus_closed_even (n m: El even): Prf (even_p ((fst n) + (fst m)))
+symbol plus_closed_even (n m: El even): Prf (even_p ((fst n) + (fst m)));
 
 symbol add (n m: El even) : El even
-     ≔ pair ((fst n) + (fst m)) (plus_closed_even n m)
+     ≔ pair ((fst n) + (fst m)) (plus_closed_even n m);
 
-symbol plus_commutativity (n m: El â„•): Prf (n + m = m + n)
+symbol plus_commutativity (n m: El â„•): Prf (n + m = m + n);
 
 opaque symbol even_add_commutativity (n m: El even)
             : Prf (eqEven (add n m) (add m n))
             ≔
 begin
-  assume n m
-  refine plus_commutativity (fst n) (fst m)
-end
+  assume n m;
+  refine plus_commutativity (fst n) (fst m);
+end;
diff --git a/paper/stack.lp b/paper/stack.lp
index 8e7c779e5edfb2af520f540d5498f7eb82feda58..ddae3b9d363f0df51f26f7c7fb1a1cea0d579c10 100644
--- a/paper/stack.lp
+++ b/paper/stack.lp
@@ -1,27 +1,27 @@
 require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.logical
-require open personoj.encodings.equality
+             personoj.encodings.pvs_cert
+             personoj.encodings.logical
+             personoj.encodings.equality;
 
-constant symbol stack: Set
-constant symbol empty: El stack
+constant symbol stack: Set;
+constant symbol empty: El stack;
 
-definition nonempty_stack_p (s: El stack) ≔ ¬ (s = empty)
-definition nonempty_stack ≔ psub nonempty_stack_p
+symbol nonempty_stack_p (s: El stack) ≔ ¬ (s = empty);
+symbol nonempty_stack ≔ psub nonempty_stack_p;
 
-constant symbol t: Set
-symbol push: El t → El stack → El nonempty_stack
-symbol pop: El nonempty_stack → El stack
-symbol top: El nonempty_stack → El t
+constant symbol t: Set;
+symbol push: El t → El stack → El nonempty_stack;
+symbol pop: El nonempty_stack → El stack;
+symbol top: El nonempty_stack → El t;
 
 symbol push_top_pop (s: El stack) (hn: Prf (nonempty_stack_p s))
      : let sne ≔ pair s hn in
-       Prf ((push (top sne) (pop sne)) = sne)
+       Prf ((push (top sne) (pop sne)) = sne);
 
-rule pop (push _ $s) ↪ $s
-rule top (push $x _) ↪ $x
-symbol pop_push (x: El t) (s: El stack): Prf ((pop (push x s)) = s)
-symbol top_push (x: El t) (s: El stack): Prf ((top (push x s)) = x)
+rule pop (push _ $s) ↪ $s;
+rule top (push $x _) ↪ $x;
+symbol pop_push (x: El t) (s: El stack): Prf ((pop (push x s)) = s);
+symbol top_push (x: El t) (s: El stack): Prf ((top (push x s)) = x);
 
 // The following theorem has unsolved meta variables
 // theorem pop2push2 (x y: El t) (s: El stack)