diff --git a/theories/compile.v b/theories/compile.v
index 3eaaf42..f063b16 100644
--- a/theories/compile.v
+++ b/theories/compile.v
@@ -66,6 +66,18 @@ Module Join.
   Lemma UnivInj n i j : R (Univ i : Tm n) (Univ j) -> i = j.
   Proof. hauto l:on use:join_univ_inj. Qed.
 
+  Lemma transitive n (a b c : Tm n) :
+    R a b -> R b c -> R a c.
+  Proof. hauto l:on use:join_transitive unfold:R. Qed.
+
+  Lemma symmetric n (a b : Tm n) :
+    R a b -> R b a.
+  Proof. hauto l:on use:join_symmetric. Qed.
+
+  Lemma reflexive n (a : Tm n) :
+    R a a.
+  Proof. hauto l:on use:join_refl. Qed.
+
 End Join.
 
 Module Equiv.
@@ -135,3 +147,6 @@ Module EquivJoin.
     - hauto l:on.
   Qed.
 End EquivJoin.
+
+Module CompilePar.
+End CompilePar.
diff --git a/theories/logrel.v b/theories/logrel.v
index a421cda..c822d06 100644
--- a/theories/logrel.v
+++ b/theories/logrel.v
@@ -344,7 +344,7 @@ Proof.
   sfirstorder.
 Qed.
 
-#[export]Hint Resolve join_univ_ne_contra join_bind_ne_contra join_univ_pi_contra join_symmetric join_transitive : join.
+#[export]Hint Resolve join_univ_ne_contra join_bind_ne_contra join_univ_pi_contra Join.symmetric Join.transitive : join.
 
 Lemma InterpExt_Join n i I (A B : Tm n) PA PB :
   ⟦ A ⟧ i ;; I ↘ PA ->