diff --git a/personoj/builtins.lp b/personoj/builtins.lp
index 360baa80568baf02304dc137d4951870951b1501..ddda077c38fb0b88ca98259a6abc86265f4ff676 100644
--- a/personoj/builtins.lp
+++ b/personoj/builtins.lp
@@ -23,4 +23,5 @@ constant symbol str_cons: El {|!Number!|} → El {|!String!|} → El {|!String!|
 symbol ∃ {T: Set} (P: El T → El prop) ≔ ¬ (∀ (λ x, ¬ (P x)));
 
 symbol propositional_extensionality:
-  Prf (∀ {prop} (λ p, (∀ {prop} (λ q, (iff p q) ⊃ (λ _, eq {prop} (cons p q))))));
+  Prf (∀ (λ p: El prop,
+          (∀ (λ q: El prop, (iff p q) ⇒ (λ _, eq {prop} (cons p q))))));
diff --git a/personoj/examples/stack.lp b/personoj/examples/stack.lp
index 2218f4532ac203c633f9915c9261e6e0db69dcca..4573a6acabcfec3909521a145a0bb9c3dc425e42 100644
--- a/personoj/examples/stack.lp
+++ b/personoj/examples/stack.lp
@@ -1,33 +1,39 @@
-require open personoj.lhol
-             personoj.pvs_cert
-             personoj.logical
-             personoj.eqtup;
+require open personoj.lhol personoj.pvs_cert personoj.logical personoj.eqtup;
+require open personoj.coercions;
 
 // Get currified infix equality
 require open personoj.extra.equality;
 
-constant symbol stack: Set;
-constant symbol empty: El stack;
+constant symbol stack {_: Set}: Set;
+constant symbol empty {t: Set}: El (stack {t});
 
-symbol nonempty_stack_p (s: El stack) ≔ ¬ (s = empty);
-symbol nonempty_stack ≔ psub nonempty_stack_p;
+symbol nonempty_stack? {t: Set} (s: El (stack {t})) ≔ s ≠ empty {t};
+symbol nonempty_stack {t: Set} ≔ psub (nonempty_stack? {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;
+constant symbol push {t: Set}: El t → El (stack {t}) → El (nonempty_stack {t});
+constant symbol pop {t: Set}: El (nonempty_stack {t}) → El (stack {t});
+constant symbol top {t: Set}: El (nonempty_stack {t}) → 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);
+symbol push_top_pop {t: Set}:
+  Prf (∀ (λ s: El (stack {t}),
+          nonempty_stack? {t} s ⇒ (λ nes, push (top s) (pop s) = s)))
+begin
+  // Solve TCCs
+  refine nes;
+  refine nes;
+  refine nes;
+end;
 
-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);
+constant symbol pop_push {t: Set}:
+  Prf (∀ (λ s: El (stack {t}), ∀ (λ x: El t, pop (push x s) = s)));
 
-// The following theorem has unsolved meta variables
-// theorem pop2push2 (x y: El t) (s: El stack)
-//       : Prf (pop (pair (pop (push x (fst (push y s)))) _) = s)
-// proof
-// qed
+constant symbol top_push {t: Set}:
+  Prf (∀ (λ s: El (stack {t}), ∀ (λ x: El t, top (push x s) = x)));
+
+opaque symbol pop2push2 {t: Set}:
+  Prf (∀ (λ s: El (stack {t}),
+          ∀ (λ x: El t,
+            (∀ (λ y: El t, pop (pop (push x (push y s))) = s))))) ≔
+begin
+  admit;
+end;
diff --git a/personoj/extra/bool_plus.lp b/personoj/extra/bool_plus.lp
index 87ab607cd9f5df0a3d465755904ea7cd2c4b4f81..1eb48fb52c1c3c31ea5cae70cc594ef4cde168b8 100644
--- a/personoj/extra/bool_plus.lp
+++ b/personoj/extra/bool_plus.lp
@@ -7,7 +7,7 @@ symbol and_intro:
   Prf
   (∀ {prop} (λ a,
    ∀ {prop} (λ b,
-   a ⊃ (λ _, b ⊃ (λ _, a ∧ (λ _, b)))))) ≔
+   a ⇒ (λ _, b ⇒ (λ _, a ∧ (λ _, b)))))) ≔
 begin
   assume A B h0 h1 f;
   refine f h0 h1;
diff --git a/personoj/logical.lp b/personoj/logical.lp
index 72014bcb8dd8afa38985b771e2e3e26bebac71c8..cf7f528b644eb87e1b125fb6f53ccb29d9ac4ebc 100644
--- a/personoj/logical.lp
+++ b/personoj/logical.lp
@@ -1,31 +1,14 @@
 // Definition based on implication
 require open personoj.lhol;
 
+symbol ⇒ P Q ≔ impd {P} Q;             notation ⇒ infix right 2;
 symbol false ≔ ∀ {prop} (λ x, x);
-symbol true ≔ impd {false} (λ _, false);
-
-symbol not P ≔ impd {P} (λ _, false);
-symbol ¬ ≔ not;
-notation ¬ prefix 5;
-
-symbol imp P Q ≔ impd {P} Q;
-symbol ⊃ ≔ imp;
-notation ⊃ infix right 2;
-
-symbol and P Q ≔ ¬ (P ⊃ (λ h, ¬ (Q h)));
-symbol or P Q ≔ (¬ P) ⊃ Q;
-symbol ∧ ≔ and; symbol ∨ ≔ or;
-notation ∧ infix 4;
-notation ∨ infix 3;
-
-builtin "bot" ≔ false;
-builtin "top" ≔ true;
-builtin "not" ≔ not;
-builtin "imp" ≔ imp;
-builtin "and" ≔ and;
-builtin "or"  ≔ or;
+symbol true ≔ false ⇒ (λ _, false);
+symbol ¬ P ≔ impd {P} (λ _, false);    notation ¬ prefix 5;
+symbol ∧ P Q ≔ ¬ (P ⇒ (λ h, ¬ (Q h))); notation ∧ infix 4;
+symbol ∨ P Q ≔ (¬ P) ⇒ Q;              notation ∨ infix 3;
 
 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);
+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));