diff --git a/HahnEquational.v b/HahnEquational.v
index b785b0e..b9d9621 100644
--- a/HahnEquational.v
+++ b/HahnEquational.v
@@ -134,6 +134,10 @@ Lemma same_relation_exp A (r r' : relation A) (EQ: r ≡ r') :
   forall x y, r x y <-> r' x y.
 Proof. split; apply EQ. Qed.
 
+Lemma same_relation_exp' A (r r' : relation A) (EQ: forall x y, r x y <-> r' x y):
+  r ≡ r'. 
+Proof. red. split; red; ins; by apply EQ. Qed.
+
 Lemma same_relation_refl A : reflexive (@same_relation A).
 Proof. u. Qed.
 
diff --git a/HahnSets.v b/HahnSets.v
index 6e46642..fbf30cb 100644
--- a/HahnSets.v
+++ b/HahnSets.v
@@ -284,6 +284,10 @@ Section SetProperties.
   Lemma set_subset_collect f s s' (S: s ⊆₁ s') : f ↑₁ s ⊆₁ f ↑₁ s'.
   Proof. u. Qed.
 
+  Lemma set_minus_subset s s':
+    s \₁ s' ⊆₁ s.
+  Proof. u. Qed. 
+
   (** Properties of set equivalence. *)
 
   Lemma set_equivE s s' : s ≡₁ s' <-> s ⊆₁ s' /\ s' ⊆₁ s.
@@ -326,6 +330,10 @@ Section SetProperties.
   Lemma set_equiv_exp s s' (EQ: s ≡₁ s') : forall x, s x <-> s' x.
   Proof. split; apply EQ. Qed.
 
+  Lemma set_equiv_exp' s s' (EQ: forall x, s x <-> s' x):
+    s ≡₁ s'. 
+  Proof. red. split; red; ins; by apply EQ. Qed.
+
   (** Absorption properties. *)
 
   Lemma set_union_absorb_l s s' (SUB: s ⊆₁ s') : s ∪₁ s' ≡₁ s'.
@@ -516,6 +524,14 @@ Section SetProperties.
     eexists findom0; ins; desf; apply IHfindom; eexists; splits; eauto; congruence.
   Qed.
 
+  Lemma set_finite_minus s s' (FIN: set_finite s):
+    set_finite (s \₁ s').
+  Proof. u. Qed.
+  
+  Lemma set_finite_inter s s' (FIN: set_finite s):
+    set_finite (s ∩₁ s').
+  Proof. u. Qed.
+
   (** Set disjointness *)
 
   Lemma set_disjointE s s' : set_disjoint s s' <-> s ∩₁ s' ≡₁ ∅.
diff --git a/HahnTrace.v b/HahnTrace.v
index 4f08f7d..7e24285 100644
--- a/HahnTrace.v
+++ b/HahnTrace.v
@@ -764,6 +764,19 @@ Section LTS_traces.
     exists fl'; split; ins.
   Qed.
 
+  Lemma LTS_traceE' t
+        (DOM: exists fl',
+            LTS_init lts (fl' 0) /\
+            (forall i,
+                NOmega.lt_nat_l i (trace_length t) ->
+                forall d, LTS_step lts (fl' i) (trace_nth i t d) (fl' (S i)))):
+    LTS_trace t.
+  Proof.
+    ins. desc. red.
+    destruct t; [by vauto| ].
+    simpl in *. exists fl'. split; intuition.
+  Qed.
+
 End LTS_traces.