diff --git a/adlib/subtype.lp b/adlib/subtype.lp
index 6e0492e27f3a45c1f044fa17375f7808eeb4c3db..ae3b19569006e2cf70921ec41414602fb95ba391 100644
--- a/adlib/subtype.lp
+++ b/adlib/subtype.lp
@@ -1,5 +1,5 @@
 require open personoj.encodings.cert_f
-personoj.adlib.bootstrap
+        personoj.adlib.bootstrap
 
 // A la rewriting logic
 rule Psub {&A} _ ⊑ &A → true
diff --git a/prelude/logic.lp b/prelude/logic.lp
index ef6be7110053238a7fff0b7275300752ef4b888d..2d062b3f021df622dc6a0142f3bd36e33c09302e 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -106,10 +106,10 @@ symbol reflexivity_of_equal T (x: Term T) : Term (eq x x)
 // set builtin "refl" ≔ reflexivity_of_equal
 
 symbol transitivity_of_equal T (x y z: Term T) :
-  Term ((eq x y) ∧ (eq y z)) ⇒ Term (eq x z)
+  Term ((x = y) ∧ (y = z)) ⇒ Term (eq x z)
 
 symbol symmetry_of_equal T (x y: Term T):
-  Term (eq x y) ⇒ Term (eq y x)
+  Term (x = y) ⇒ Term (y = x)
 
 //
 // if_props
diff --git a/sandbox/nat.lp b/sandbox/nat.lp
index dfa720e31a834f83287c5284f0f4047fef1c3c72..f714630b34eef606d5a5475886d81397cf37a1af 100644
--- a/sandbox/nat.lp
+++ b/sandbox/nat.lp
@@ -62,7 +62,10 @@ qed
 symbol surjective_pairing T (p: Term T ⇒ Term bool):
        ∀x: Term (Psub p), Term (pair p (fst x) (snd x) = x)
 
-theorem prf_irrelevance: ∀x y: Term Even, Term (fst x = fst y) ⇒ Term (x = y)
+//symbol app_thm (D R: Term uType) (f: Term (D ~> R))
+//     : ∀x y: Term D, Term (x = y) ⇒ Term (f x = f y)
+
+theorem fst_injective: ∀x y: Term Even, Term (fst x = fst y) ⇒ Term (x = y)
 proof
     assume x y h
     refine transitivity_of_equal Even x (pair even (fst x) (snd x)) y _
@@ -79,5 +82,14 @@ proof
     focus 1
     refine surjective_pairing _ even y
 
-    simpl //FIXME
+abort
+
+rule &x = &x → true
+theorem prf_irrelevance T (p: Term T ⇒ Term bool)
+: ∀(x: Term T) (pr: Term (p x)) (pr': Term (p x)), Term (pair p x pr = pair p x pr')
+proof
+    assume T p x pr0 pr1
+    simpl
+    assume h
+    refine h
 qed
diff --git a/sandbox/rat.lp b/sandbox/rat.lp
index 547492f1934b6680c144a188b5af1b140b50e9de..cab1f9924923ef74704a71a963ae4e2d36097c61 100644
--- a/sandbox/rat.lp
+++ b/sandbox/rat.lp
@@ -16,8 +16,6 @@ set infix 8 "/" ≔ rat
 
 symbol times : Term Rat ⇒ Term Rat ⇒ Term Rat
 
-type λx: Term N.Nznat, fst x
-
 rule times (rat &a &b) (rat &c &d) →
   let bv ≔ fst &b in
   let dv ≔ fst &d in