diff --git a/theories/bunch_decomp.v b/theories/bunch_decomp.v
index 713563e..5d2d505 100644
--- a/theories/bunch_decomp.v
+++ b/theories/bunch_decomp.v
@@ -162,3 +162,152 @@ Proof.
         rewrite fn_lookup_insert_ne//.
       * apply HH.
 Qed.
+
+Local Lemma bunch_equiv_fill_1 {formula} (Δ : @bunch formula) C ϕ :
+  fill C (frml ϕ) =? Δ →
+  ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill C Δ).
+Proof.
+  intros Heq.
+  remember (fill C (frml ϕ)) as Y.
+  revert C HeqY.
+  induction Heq=>C' heqY; symmetry in heqY.
+  + apply bunch_decomp_complete in heqY.
+    apply bunch_decomp_ctx in heqY.
+    destruct heqY as [H1 | H2].
+    * destruct H1 as [C1 [HC0%bunch_decomp_correct HC]].
+      destruct (IHHeq C1 HC0) as [C2 [HΔ1 HC2]].
+      simplify_eq/=.
+      exists (C2 ++ C). rewrite fill_app. split; first done.
+      intros Δ. rewrite !fill_app HC2 //.
+    * destruct H2 as (C1 & C2 & HC1 & HC2 & Hdec0).
+      specialize (Hdec0 Δ2). apply bunch_decomp_correct in Hdec0.
+      exists (C1 Δ2). split ; eauto.
+      intros Δ. rewrite HC1.
+      assert (Δ1 ≡ Δ2) as <-.
+      { by apply rtsc_lr. }
+      by rewrite HC2.
+  + apply bunch_decomp_complete in heqY.
+    inversion heqY; simplify_eq/=.
+    { inversion H4. }
+    apply bunch_decomp_correct in H4.
+    exists Π. split; eauto.
+    intros X. rewrite fill_app /= left_id //.
+  + apply bunch_decomp_complete in heqY.
+    inversion heqY; simplify_eq/=.
+    * exists (Π ++ [CtxR s Δ2]). split.
+      { rewrite fill_app/=.
+        apply bunch_decomp_correct in H4.
+        by rewrite H4. }
+      intros Δ. rewrite !fill_app/=.
+      by rewrite comm.
+    * exists (Π ++ [CtxL s Δ1]). split.
+      { rewrite fill_app/=.
+        apply bunch_decomp_correct in H4.
+        by rewrite H4. }
+      intros Δ. rewrite !fill_app/=.
+      by rewrite comm.
+  + apply bunch_decomp_complete in heqY.
+    inversion heqY; simplify_eq/=.
+    * exists (Π ++ [CtxL s Δ2;CtxL s Δ3])%B. split.
+      { rewrite fill_app/=.
+        apply bunch_decomp_correct in H4.
+        by rewrite H4. }
+      intros Δ. rewrite !fill_app/=.
+      by rewrite assoc.
+    * inversion H4; simplify_eq/=.
+      ** exists (Π0 ++ [CtxR s Δ1;CtxL s Δ3])%B. split.
+         { rewrite fill_app/=.
+           apply bunch_decomp_correct in H5.
+           by rewrite H5. }
+         intros Δ. rewrite !fill_app/=.
+         by rewrite assoc.
+      ** exists (Π0 ++ [CtxR s (bbin s Δ1 Δ2)])%B. split.
+         { simpl. rewrite fill_app/=.
+           apply bunch_decomp_correct in H5.
+           by rewrite H5. }
+         intros Δ. rewrite !fill_app/=.
+         by rewrite assoc.
+Qed.
+
+Local Lemma bunch_equiv_fill_2 {formula} (Δ : @bunch formula) C ϕ :
+  Δ =? fill C (frml ϕ) →
+  ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill C Δ).
+Proof.
+  intros Heq.
+  remember (fill C (frml ϕ)) as Y.
+  revert C HeqY.
+  induction Heq=>C' heqY; symmetry in heqY.
+  + apply bunch_decomp_complete in heqY.
+    apply bunch_decomp_ctx in heqY.
+    destruct heqY as [H1 | H2].
+    * destruct H1 as [C1 [HC0%bunch_decomp_correct HC]].
+      destruct (IHHeq C1 HC0) as [C2 [HΔ1 HC2]].
+      simplify_eq/=.
+      exists (C2 ++ C). rewrite fill_app. split; first done.
+      intros Δ. rewrite !fill_app HC2 //.
+    * destruct H2 as (C1 & C2 & HC1 & HC2 & Hdec0).
+      specialize (Hdec0 Δ1). apply bunch_decomp_correct in Hdec0.
+      exists (C1 Δ1). split ; eauto.
+      intros Δ. rewrite HC1.
+      assert (Δ1 ≡ Δ2) as ->.
+      { by apply rtsc_lr. }
+      by rewrite HC2.
+  + exists (C' ++ [CtxR s (bnul s)]%B). simpl; split.
+    { rewrite fill_app /=. by rewrite heqY. }
+    intros X; rewrite fill_app/=.
+    by rewrite left_id.
+  + apply bunch_decomp_complete in heqY.
+    inversion heqY; simplify_eq/=.
+    * exists (Π ++ [CtxR s Δ1]). split.
+      { rewrite fill_app/=.
+        apply bunch_decomp_correct in H4.
+        by rewrite H4. }
+      intros Δ. rewrite !fill_app/=.
+      by rewrite comm.
+    * exists (Π ++ [CtxL s Δ2]). split.
+      { rewrite fill_app/=.
+        apply bunch_decomp_correct in H4.
+        by rewrite H4. }
+      intros Δ. rewrite !fill_app/=.
+      by rewrite comm.
+  + apply bunch_decomp_complete in heqY.
+    inversion heqY; simplify_eq/=.
+    * inversion H4; simplify_eq/=.
+      ** exists (Π0 ++ [CtxL s (bbin s Δ2 Δ3)])%B. split.
+         { rewrite fill_app/=.
+           apply bunch_decomp_correct in H5.
+           by rewrite H5. }
+         intros Δ. rewrite !fill_app/=.
+         by rewrite assoc.
+      ** exists (Π0 ++ [CtxL s Δ3;CtxR s Δ1])%B. split.
+         { simpl. rewrite fill_app/=.
+           apply bunch_decomp_correct in H5.
+           by rewrite H5. }
+         intros Δ. rewrite !fill_app/=.
+         by rewrite assoc.
+    * exists (Π ++ [CtxR s Δ2;CtxR s Δ1])%B. split.
+      { rewrite fill_app/=.
+        apply bunch_decomp_correct in H4.
+        by rewrite H4. }
+      intros Δ. rewrite !fill_app/=.
+      by rewrite assoc.
+Qed.
+
+Lemma bunch_equiv_fill {formula} Δ C (ϕ : formula) :
+  Δ ≡ (fill C (frml ϕ)) →
+  ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill C Δ).
+Proof.
+  revert Δ. eapply rtc_ind_l.
+  { exists C. eauto. }
+  intros X Y HXY HY. clear HY.
+  intros (C0 & -> & HC0).
+  destruct HXY as [HXY|HXY].
+  - apply bunch_equiv_fill_2 in HXY.
+    destruct HXY as (C' & -> & HC').
+    eexists; split; eauto.
+    intros ?. by rewrite HC' HC0.
+  - apply bunch_equiv_fill_1 in HXY.
+    destruct HXY as (C' & -> & HC').
+    eexists; split; eauto.
+    intros ?. by rewrite HC' HC0.
+Qed.
diff --git a/theories/bunches.v b/theories/bunches.v
index 8c50532..eb7a059 100644
--- a/theories/bunches.v
+++ b/theories/bunches.v
@@ -72,15 +72,14 @@ Definition bunch_ctx_map {A B} (f : A → B) (Π : @bunch_ctx A) := map (bunch_c
 (** Equivalence on bunches is defined to be the least congruence
       that satisfies the monoidal laws for (empty and comma) and (top
       and semicolon). *)
-Inductive bunch_equiv {frml} : @bunch frml → @bunch frml → Prop :=
-| BE_refl Δ : Δ =? Δ
-| BE_sym Δ1 Δ2 : Δ1 =? Δ2 → Δ2 =? Δ1
-| BE_trans Δ1 Δ2 Δ3 : Δ1 =? Δ2 → Δ2 =? Δ3 → Δ1 =? Δ3
+Inductive bunch_equiv_step {frml} : @bunch frml → @bunch frml → Prop :=
 | BE_cong C Δ1 Δ2 : Δ1 =? Δ2 → fill C Δ1 =? fill C Δ2
 | BE_unit_l s Δ : bbin s (bnul s) Δ =? Δ
 | BE_comm s Δ1 Δ2 : bbin s Δ1 Δ2 =? bbin s Δ2 Δ1
 | BE_assoc s Δ1 Δ2 Δ3 : bbin s Δ1 (bbin s Δ2 Δ3) =? bbin s (bbin s Δ1 Δ2) Δ3
-where "Δ =? Γ" := (bunch_equiv Δ%B Γ%B).
+where "Δ =? Γ" := (bunch_equiv_step Δ%B Γ%B).
+
+Definition bunch_equiv {frml} := rtsc (@bunch_equiv_step frml).
 
 (** Register [bunch_equiv] as [(≡)] *)
 #[export] Instance equiv_bunch_equiv frml : Equiv (@bunch frml) := bunch_equiv.
@@ -88,34 +87,34 @@ where "Δ =? Γ" := (bunch_equiv Δ%B Γ%B).
 (** * Properties *)
 
 #[export] Instance equivalence_bunch_equiv frml : Equivalence ((≡@{@bunch frml})).
-Proof.
-  repeat split.
-  - intro x. econstructor.
-  - intros x y Hxy. by econstructor.
-  - intros x y z Hxy Hyz. by econstructor.
-Qed.
+Proof. apply _. Qed.
 
 #[export] Instance bbin_comm frml s : Comm (≡@{@bunch frml}) (bbin s).
-Proof. intros X Y. apply BE_comm. Qed.
+Proof. intros X Y. apply rtsc_rl. apply BE_comm. Qed.
 #[export] Instance bbin_assoc frml s : Assoc (≡@{@bunch frml}) (bbin s).
-Proof. intros X Y Z. apply BE_assoc. Qed.
+Proof. intros X Y Z. apply rtsc_lr. apply BE_assoc. Qed.
 #[export] Instance bbin_leftid frml s : LeftId (≡@{@bunch frml}) (bnul s) (bbin s).
-Proof. intros X. apply BE_unit_l. Qed.
+Proof. intros X. apply rtsc_lr. apply BE_unit_l. Qed.
 #[export] Instance bbin_rightid frml s : RightId (≡@{@bunch frml}) (bnul s) (bbin s).
-Proof. intros X. rewrite comm. apply BE_unit_l. Qed.
+Proof. intros X. rewrite comm. apply rtsc_lr. apply BE_unit_l. Qed.
 
 #[export] Instance fill_proper frml Π : Proper ((≡) ==> (≡@{@bunch frml})) (fill Π).
-Proof. intros X Y. apply BE_cong. Qed.
+Proof.
+  intros X Y.
+  eapply rtc_congruence. clear X Y.
+  intros X Y. apply sc_congruence. clear X Y.
+  intros X Y ?. by econstructor.
+Qed.
 
 #[export] Instance bbin_proper frml s : Proper ((≡) ==> (≡) ==> (≡@{@bunch frml})) (bbin s).
 Proof.
   intros Δ1 Δ2 H Δ1' Δ2' H'.
   change ((fill [CtxL s Δ1'] Δ1) ≡ (fill [CtxL s Δ2'] Δ2)).
   etrans.
-  { eapply BE_cong; eauto. }
+  { eapply fill_proper; eauto. }
   simpl.
   change ((fill [CtxR s Δ2] Δ1') ≡ (fill [CtxR s Δ2] Δ2')).
-  eapply BE_cong; eauto.
+  eapply fill_proper; eauto.
 Qed.
 
 Lemma fill_app {frml} (Π Π' : @bunch_ctx frml) (Δ : bunch) :
@@ -129,16 +128,26 @@ Proof.
   rewrite IH. f_equiv. by destruct F; simpl.
 Qed.
 
-Global Instance bunch_map_proper {A B} (f : A → B) : Proper ((≡) ==> (≡@{bunch})) (fmap f).
+Lemma bunch_map_proper' {A B} (f : A → B) : Proper ((bunch_equiv_step) ==> (≡@{bunch})) (fmap f).
 Proof.
-  intros Δ1 Δ2 HD. induction HD; simpl; eauto.
-  - etrans; eauto.
-  - rewrite !bunch_map_fill. by f_equiv.
+  intros Δ1 Δ2 HD.
+  induction HD; simpl.
+  - rewrite !bunch_map_fill; by f_equiv.
   - by rewrite left_id.
   - by rewrite comm.
   - by rewrite assoc.
 Qed.
 
+#[global] Instance bunch_map_proper {A B} (f : A → B) : Proper ((≡) ==> (≡@{bunch})) (fmap f).
+Proof.
+  intros Δ1 Δ2 HD.
+  induction HD as [|Δ1 Δ2 Δ3 HD1 HD]; first done.
+  etrans; last by apply IHHD.
+  destruct HD1 as [HD1 | HD1].
+  - by apply bunch_map_proper'.
+  - symmetry. by apply bunch_map_proper'.
+Qed.
+
 Section interp.
   Variable (PROP : bi).
   Context {formula : Type}.
@@ -237,10 +246,9 @@ Section interp.
       apply (IHΠ (λ i, bunch_interp Δ1 ∧ P i)%I).
   Qed.
 
-  Global Instance bunch_interp_proper : Proper ((≡) ==> (≡)) bunch_interp.
+  Lemma bunch_interp_proper' : Proper ((bunch_equiv_step) ==> (≡)) bunch_interp.
   Proof.
     intros Δ1 Δ2. induction 1; eauto.
-    - etrans; eassumption.
     - apply bi.equiv_entails_2.
       + apply bunch_interp_fill_mono; eauto.
         by apply bi.equiv_entails_1_1.
@@ -251,6 +259,13 @@ Section interp.
     - simpl. destruct s; by rewrite assoc.
   Qed.
 
+  #[global] Instance bunch_interp_proper : Proper ((≡) ==> (≡)) bunch_interp.
+  Proof.
+    intros Δ1 Δ2. induction 1 as [|Δ1 Δ2 Δ3 HD1 HD]; first done.
+    etrans; last by eassumption.
+    destruct HD1; [| symmetry]; by apply bunch_interp_proper'.
+  Qed.
+
   Global Instance bunch_ctx_interp_mono Π : Proper ((⊢) ==> (⊢)) (bunch_ctx_interp Π).
   Proof.
     induction Π as [|F Π]=>P1 P2 HP; first by simpl; auto.
diff --git a/theories/s4/cutelim.v b/theories/s4/cutelim.v
index a32440e..bc94f3e 100644
--- a/theories/s4/cutelim.v
+++ b/theories/s4/cutelim.v
@@ -310,7 +310,7 @@ Qed.
 Lemma box_true : True ⊢@{C_alg} C_box (True : C_alg).
 Proof.
   apply cl_adj. { apply _. } intros Δ _.
-  rewrite -(BE_unit_l _ Δ).
+  rewrite -(left_id ∅ₐ%B _ Δ).
   apply C_weaken. apply (cl_unit _ _ _).
   simpl. exists ∅ₐ%B. simpl. split; auto.
   apply (cl_unit _ _ _). done.
diff --git a/theories/s4/seqcalc_height.v b/theories/s4/seqcalc_height.v
index 88f0e38..5d5a94b 100644
--- a/theories/s4/seqcalc_height.v
+++ b/theories/s4/seqcalc_height.v
@@ -16,270 +16,6 @@ Section SeqcalcHeight.
   Implicit Type Δ : bunch.
   Implicit Type ψ ϕ : formula.
 
-  (** ** Alternative formulation of bunch equivalences *)
-  Inductive bunch_equiv : bunch → bunch → Prop :=
-  | BE_cong Π Δ1 Δ2 :
-      Δ1 =? Δ2 →
-      fill Π Δ1 =? fill Π Δ2
-  | BE_comma_unit_l Δ :
-      (∅ₘ ,, Δ)%B =? Δ
-  | BE_comma_comm Δ1 Δ2 :
-      (Δ1 ,, Δ2)%B =? (Δ2 ,, Δ1)%B
-  | BE_comma_assoc Δ1 Δ2 Δ3 : (Δ1 ,, (Δ2 ,, Δ3))%B =? ((Δ1 ,, Δ2) ,, Δ3)%B
-  | BE_semic_unit_l Δ : (∅ₐ ;, Δ)%B =? Δ
-  | BE_semic_comm Δ1 Δ2  : (Δ1 ;, Δ2)%B =? (Δ2 ;, Δ1)%B
-  | BE_semic_assoc Δ1 Δ2 Δ3  : (Δ1 ;, (Δ2 ;, Δ3))%B =? ((Δ1 ;, Δ2) ;, Δ3)%B
-  where "Δ =? Γ" := (bunch_equiv Δ%B Γ%B).
-
-  Definition bunch_equiv_h := rtsc (bunch_equiv).
-
-  Lemma bunch_equiv_1 Δ Δ' :
-    (Δ =? Δ') → (Δ ≡ Δ').
-  Proof. induction 1; by econstructor; eauto. Qed.
-
-  Lemma bunch_equiv_2 Δ Δ' :
-    (Δ ≡ Δ') → (bunch_equiv_h Δ Δ').
-  Proof.
-    induction 1.
-    all: try by (eapply rtsc_lr; destruct s; econstructor).
-    - unfold bunch_equiv_h. reflexivity.
-    - by symmetry.
-    - etrans; eauto.
-    - eapply rtc_congruence; eauto.
-      intros X Y. apply sc_congruence. clear X Y.
-      intros X Y ?. by econstructor.
-  Qed.
-
-  Local Lemma bunch_equiv_fill_1 Δ Π ϕ :
-    fill Π (frml ϕ) =? Δ →
-    ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill Π Δ).
-  Proof.
-    intros Heq.
-    remember (fill Π (frml ϕ)) as Y.
-    revert Π HeqY.
-    induction Heq=>C' heqY; symmetry in heqY.
-    + apply bunch_decomp_complete in heqY.
-      apply bunch_decomp_ctx in heqY.
-      destruct heqY as [H1 | H2].
-      * destruct H1 as [C1 [HC0%bunch_decomp_correct HC]].
-        destruct (IHHeq C1 HC0) as [C2 [HΔ1 HC2]].
-        simplify_eq/=.
-        exists (C2 ++ Π). rewrite fill_app. split; first done.
-        intros Δ. rewrite !fill_app HC2 //.
-      * destruct H2 as (C1 & C2 & HC1 & HC2 & Hdec0).
-        specialize (Hdec0 Δ2). apply bunch_decomp_correct in Hdec0.
-        exists (C1 Δ2). split ; eauto.
-        intros Δ. rewrite HC1.
-        assert (Δ1 ≡ Δ2) as <-.
-        { by apply bunch_equiv_1. }
-        by rewrite HC2.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      { inversion H4. }
-      apply bunch_decomp_correct in H4.
-      exists Π. split; eauto.
-      intros X. rewrite fill_app /= left_id //.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * exists (Π ++ [CtxCommaR Δ2]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-      * exists (Π ++ [CtxCommaL Δ1]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * exists (Π ++ [CtxCommaL Δ2;CtxCommaL Δ3])%B. split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite assoc.
-      * inversion H4; simplify_eq/=.
-        ** exists (Π0 ++ [CtxCommaR Δ1;CtxCommaL Δ3])%B. split.
-           { rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-        ** exists (Π0 ++ [CtxCommaR (Δ1,,Δ2)])%B. split.
-           { simpl. rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      { inversion H4. }
-      apply bunch_decomp_correct in H4.
-      exists Π. split; eauto.
-      intros X. rewrite fill_app /= left_id //.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * exists (Π ++ [CtxSemicR Δ2]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-      * exists (Π ++ [CtxSemicL Δ1]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * exists (Π ++ [CtxSemicL Δ2;CtxSemicL Δ3])%B. split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite assoc.
-      * inversion H4; simplify_eq/=.
-        ** exists (Π0 ++ [CtxSemicR Δ1;CtxSemicL Δ3])%B. split.
-           { rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-        ** exists (Π0 ++ [CtxSemicR (Δ1;,Δ2)])%B. split.
-           { simpl. rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-  Qed.
-
-  Local Lemma bunch_equiv_fill_2 Δ Π ϕ :
-    Δ =? fill Π (frml ϕ) →
-    ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill Π Δ).
-  Proof.
-    intros Heq.
-    remember (fill Π (frml ϕ)) as Y.
-    revert Π HeqY.
-    induction Heq=>C' heqY; symmetry in heqY.
-    + apply bunch_decomp_complete in heqY.
-      apply bunch_decomp_ctx in heqY.
-      destruct heqY as [H1 | H2].
-      * destruct H1 as [C1 [HC0%bunch_decomp_correct HC]].
-        destruct (IHHeq C1 HC0) as [C2 [HΔ1 HC2]].
-        simplify_eq/=.
-        exists (C2 ++ Π). rewrite fill_app. split; first done.
-        intros Δ. rewrite !fill_app HC2 //.
-      * destruct H2 as (C1 & C2 & HC1 & HC2 & Hdec0).
-        specialize (Hdec0 Δ1). apply bunch_decomp_correct in Hdec0.
-        exists (C1 Δ1). split ; eauto.
-        intros Δ. rewrite HC1.
-        assert (Δ1 ≡ Δ2) as ->.
-        { by apply bunch_equiv_1. }
-        by rewrite HC2.
-    + exists (C' ++ [CtxCommaR ∅ₘ]%B). simpl; split.
-      { rewrite fill_app /=. by rewrite heqY. }
-      intros X; rewrite fill_app/=.
-      by rewrite left_id.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * exists (Π ++ [CtxCommaR Δ1]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-      * exists (Π ++ [CtxCommaL Δ2]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * inversion H4; simplify_eq/=.
-        ** exists (Π0 ++ [CtxCommaL (Δ2 ,, Δ3)])%B. split.
-           { rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-        ** exists (Π0 ++ [CtxCommaL Δ3;CtxCommaR Δ1])%B. split.
-           { simpl. rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-      * exists (Π ++ [CtxCommaR Δ2;CtxCommaR Δ1])%B. split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-            by rewrite H4. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-    + exists (C' ++ [ CtxSemicR ∅ₐ]%B). simpl; split.
-      { rewrite fill_app /=. by rewrite heqY. }
-      intros X; rewrite fill_app/=.
-      by rewrite left_id.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * exists (Π ++ [CtxSemicR Δ1]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-      * exists (Π ++ [CtxSemicL Δ2]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * inversion H4; simplify_eq/=.
-        ** exists (Π0 ++ [CtxSemicL (Δ2 ;, Δ3)])%B. split.
-           { rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-        ** exists (Π0 ++ [CtxSemicL Δ3;CtxSemicR Δ1])%B. split.
-           { simpl. rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-      * exists (Π ++ [CtxSemicR Δ2;CtxSemicR Δ1])%B. split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-            by rewrite H4. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-  Qed.
-
-  Lemma bunch_equiv_fill Δ Π ϕ :
-    Δ ≡ (fill Π (frml ϕ)) →
-    ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill Π Δ).
-  Proof.
-    intros H%bunch_equiv_2.
-    revert Δ H. eapply rtc_ind_l.
-    { exists Π. eauto. }
-    intros X Y HXY HY. clear HY.
-    intros (C0 & -> & HC0).
-    destruct HXY as [HXY|HXY].
-    - apply bunch_equiv_fill_2 in HXY.
-      destruct HXY as (C' & -> & HC').
-      eexists; split; eauto.
-      intros ?. by rewrite HC' HC0.
-    - apply bunch_equiv_fill_1 in HXY.
-      destruct HXY as (C' & -> & HC').
-      eexists; split; eauto.
-      intros ?. by rewrite HC' HC0.
-  Qed.
-
   (** * SEQUENT CALCULUS *)
   Polymorphic Inductive proves : bunch → formula → nat → Prop :=
     (* structural *)
diff --git a/theories/seqcalc_height.v b/theories/seqcalc_height.v
index 3e89e37..86e3ac0 100644
--- a/theories/seqcalc_height.v
+++ b/theories/seqcalc_height.v
@@ -19,270 +19,6 @@ Module SeqcalcHeight(R : ANALYTIC_STRUCT_EXT).
   Implicit Type Δ : bunch.
   Implicit Type ψ ϕ : formula.
 
-  (** ** Alternative formulation of bunch equivalences *)
-  Inductive bunch_equiv : bunch → bunch → Prop :=
-  | BE_cong C Δ1 Δ2 :
-      Δ1 =? Δ2 →
-      fill C Δ1 =? fill C Δ2
-  | BE_comma_unit_l Δ :
-      (∅ₘ ,, Δ)%B =? Δ
-  | BE_comma_comm Δ1 Δ2 :
-      (Δ1 ,, Δ2)%B =? (Δ2 ,, Δ1)%B
-  | BE_comma_assoc Δ1 Δ2 Δ3 : (Δ1 ,, (Δ2 ,, Δ3))%B =? ((Δ1 ,, Δ2) ,, Δ3)%B
-  | BE_semic_unit_l Δ : (∅ₐ ;, Δ)%B =? Δ
-  | BE_semic_comm Δ1 Δ2  : (Δ1 ;, Δ2)%B =? (Δ2 ;, Δ1)%B
-  | BE_semic_assoc Δ1 Δ2 Δ3  : (Δ1 ;, (Δ2 ;, Δ3))%B =? ((Δ1 ;, Δ2) ;, Δ3)%B
-  where "Δ =? Γ" := (bunch_equiv Δ%B Γ%B).
-
-  Definition bunch_equiv_h := rtsc (bunch_equiv).
-
-  Lemma bunch_equiv_1 Δ Δ' :
-    (Δ =? Δ') → (Δ ≡ Δ').
-  Proof. induction 1; by econstructor; eauto. Qed.
-
-  Lemma bunch_equiv_2 Δ Δ' :
-    (Δ ≡ Δ') → (bunch_equiv_h Δ Δ').
-  Proof.
-    induction 1.
-    all: try by (eapply rtsc_lr; destruct s; econstructor).
-    - unfold bunch_equiv_h. reflexivity.
-    - by symmetry.
-    - etrans; eauto.
-    - eapply rtc_congruence; eauto.
-      intros X Y. apply sc_congruence. clear X Y.
-      intros X Y ?. by econstructor.
-  Qed.
-
-  Local Lemma bunch_equiv_fill_1 Δ C ϕ :
-    fill C (frml ϕ) =? Δ →
-    ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill C Δ).
-  Proof.
-    intros Heq.
-    remember (fill C (frml ϕ)) as Y.
-    revert C HeqY.
-    induction Heq=>C' heqY; symmetry in heqY.
-    + apply bunch_decomp_complete in heqY.
-      apply bunch_decomp_ctx in heqY.
-      destruct heqY as [H1 | H2].
-      * destruct H1 as [C1 [HC0%bunch_decomp_correct HC]].
-        destruct (IHHeq C1 HC0) as [C2 [HΔ1 HC2]].
-        simplify_eq/=.
-        exists (C2 ++ C). rewrite fill_app. split; first done.
-        intros Δ. rewrite !fill_app HC2 //.
-      * destruct H2 as (C1 & C2 & HC1 & HC2 & Hdec0).
-        specialize (Hdec0 Δ2). apply bunch_decomp_correct in Hdec0.
-        exists (C1 Δ2). split ; eauto.
-        intros Δ. rewrite HC1.
-        assert (Δ1 ≡ Δ2) as <-.
-        { by apply bunch_equiv_1. }
-        by rewrite HC2.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      { inversion H4. }
-      apply bunch_decomp_correct in H4.
-      exists Π. split; eauto.
-      intros X. rewrite fill_app /= left_id //.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * exists (Π ++ [CtxCommaR Δ2]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-      * exists (Π ++ [CtxCommaL Δ1]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * exists (Π ++ [CtxCommaL Δ2;CtxCommaL Δ3])%B. split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite assoc.
-      * inversion H4; simplify_eq/=.
-        ** exists (Π0 ++ [CtxCommaR Δ1;CtxCommaL Δ3])%B. split.
-           { rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-        ** exists (Π0 ++ [CtxCommaR (Δ1,,Δ2)])%B. split.
-           { simpl. rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      { inversion H4. }
-      apply bunch_decomp_correct in H4.
-      exists Π. split; eauto.
-      intros X. rewrite fill_app /= left_id //.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * exists (Π ++ [CtxSemicR Δ2]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-      * exists (Π ++ [CtxSemicL Δ1]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * exists (Π ++ [CtxSemicL Δ2;CtxSemicL Δ3])%B. split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite assoc.
-      * inversion H4; simplify_eq/=.
-        ** exists (Π0 ++ [CtxSemicR Δ1;CtxSemicL Δ3])%B. split.
-           { rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-        ** exists (Π0 ++ [CtxSemicR (Δ1;,Δ2)])%B. split.
-           { simpl. rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-  Qed.
-
-  Local Lemma bunch_equiv_fill_2 Δ C ϕ :
-    Δ =? fill C (frml ϕ) →
-    ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill C Δ).
-  Proof.
-    intros Heq.
-    remember (fill C (frml ϕ)) as Y.
-    revert C HeqY.
-    induction Heq=>C' heqY; symmetry in heqY.
-    + apply bunch_decomp_complete in heqY.
-      apply bunch_decomp_ctx in heqY.
-      destruct heqY as [H1 | H2].
-      * destruct H1 as [C1 [HC0%bunch_decomp_correct HC]].
-        destruct (IHHeq C1 HC0) as [C2 [HΔ1 HC2]].
-        simplify_eq/=.
-        exists (C2 ++ C). rewrite fill_app. split; first done.
-        intros Δ. rewrite !fill_app HC2 //.
-      * destruct H2 as (C1 & C2 & HC1 & HC2 & Hdec0).
-        specialize (Hdec0 Δ1). apply bunch_decomp_correct in Hdec0.
-        exists (C1 Δ1). split ; eauto.
-        intros Δ. rewrite HC1.
-        assert (Δ1 ≡ Δ2) as ->.
-        { by apply bunch_equiv_1. }
-        by rewrite HC2.
-    + exists (C' ++ [CtxCommaR ∅ₘ]%B). simpl; split.
-      { rewrite fill_app /=. by rewrite heqY. }
-      intros X; rewrite fill_app/=.
-      by rewrite left_id.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * exists (Π ++ [CtxCommaR Δ1]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-      * exists (Π ++ [CtxCommaL Δ2]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * inversion H4; simplify_eq/=.
-        ** exists (Π0 ++ [CtxCommaL (Δ2 ,, Δ3)])%B. split.
-           { rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-        ** exists (Π0 ++ [CtxCommaL Δ3;CtxCommaR Δ1])%B. split.
-           { simpl. rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-      * exists (Π ++ [CtxCommaR Δ2;CtxCommaR Δ1])%B. split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-            by rewrite H4. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-    + exists (C' ++ [CtxSemicR ∅ₐ]%B). simpl; split.
-      { rewrite fill_app /=. by rewrite heqY. }
-      intros X; rewrite fill_app/=.
-      by rewrite left_id.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * exists (Π ++ [CtxSemicR Δ1]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-      * exists (Π ++ [CtxSemicL Δ2]). split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-          by rewrite H4. }
-        intros Δ. rewrite !fill_app/=.
-        by rewrite comm.
-    + apply bunch_decomp_complete in heqY.
-      inversion heqY; simplify_eq/=.
-      * inversion H4; simplify_eq/=.
-        ** exists (Π0 ++ [CtxSemicL (Δ2 ;, Δ3)])%B. split.
-           { rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-        ** exists (Π0 ++ [CtxSemicL Δ3;CtxSemicR Δ1])%B. split.
-           { simpl. rewrite fill_app/=.
-             apply bunch_decomp_correct in H5.
-             by rewrite H5. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-      * exists (Π ++ [CtxSemicR Δ2;CtxSemicR Δ1])%B. split.
-        { rewrite fill_app/=.
-          apply bunch_decomp_correct in H4.
-            by rewrite H4. }
-           intros Δ. rewrite !fill_app/=.
-           by rewrite assoc.
-  Qed.
-
-  Lemma bunch_equiv_fill Δ C ϕ :
-    Δ ≡ (fill C (frml ϕ)) →
-    ∃ C', Δ = fill C' (frml ϕ) ∧ (∀ Δ, fill C' Δ ≡ fill C Δ).
-  Proof.
-    intros H%bunch_equiv_2.
-    revert Δ H. eapply rtc_ind_l.
-    { exists C. eauto. }
-    intros X Y HXY HY. clear HY.
-    intros (C0 & -> & HC0).
-    destruct HXY as [HXY|HXY].
-    - apply bunch_equiv_fill_2 in HXY.
-      destruct HXY as (C' & -> & HC').
-      eexists; split; eauto.
-      intros ?. by rewrite HC' HC0.
-    - apply bunch_equiv_fill_1 in HXY.
-      destruct HXY as (C' & -> & HC').
-      eexists; split; eauto.
-      intros ?. by rewrite HC' HC0.
-  Qed.
-
   (** * SEQUENT CALCULUS *)
   Polymorphic Inductive proves : bunch → formula → nat → Prop :=
     (* structural *)