diff --git a/theories/confluence.v b/theories/confluence.v
index da18b3c..239bac4 100644
--- a/theories/confluence.v
+++ b/theories/confluence.v
@@ -275,6 +275,170 @@ Lemma subst_id b :  subst_Tm (scons (VarTm var_zero) (funcomp VarTm shift)) b =
   case => //=.
 Qed.
 
+Module IPar.
+  Inductive R : Tm -> Tm -> Prop :=
+  | VarCong i :
+    R (VarTm i) (VarTm i)
+  | AppCong b0 b1 a0 a1 :
+    ηPar.R b0 b1 ->
+    ηPar.R a0 a1 ->
+    R (App b0 a0) (App b1 a1)
+  | AbsCong a0 a1 :
+    ηPar.R a0 a1 ->
+    R (Abs a0) (Abs a1).
+  Derive Inversion inv with (forall a b, R a b).
+
+  Lemma ToηPar a b : R a b -> ηPar.R a b.
+  Proof. induction 1; hauto lq:on ctrs:ηPar.R. Qed.
+End IPar.
+
+Module OExp.
+  Inductive R : Tm -> Tm -> Prop :=
+  | AbsEta b :
+    R b (Abs (App (ren_Tm shift b) (VarTm var_zero))).
+
+  Derive Inversion inv with (forall a b, R a b).
+End OExp.
+
+Lemma IO_factorization a c :
+  ηPar.R a c -> exists b, IPar.R a b /\ rtc OExp.R b c.
+Proof.
+  move => h. elim : a c /h.
+  - move => i. exists (VarTm i).
+    split. constructor.
+    apply rtc_refl.
+  - move => b0 b1 a0 a1 hb [b' [ihb0 ihb1]] ha [a' [iha0 iha1]].
+    exists (App b1 a1).
+    split. apply IPar.AppCong; eauto.
+    apply rtc_refl.
+  - move => a0 a1 ha [a' [iha0 iha1]].
+    exists (Abs a1). split. by apply IPar.AbsCong.
+    apply rtc_refl.
+  - move => b0 b1 hb [b' [ihb0 ihb1]].
+    exists b'. split => //.
+    apply : rtc_r; eauto.
+    constructor.
+Qed.
+
+Lemma IO_merge a b c :
+  ηPar.R a b -> OExp.R b c -> ηPar.R a c.
+Proof. hauto lq:on inv:OExp.R ctrs:ηPar.R. Qed.
+
+Lemma IO_merge' a b c :
+  ηPar.R a b -> rtc OExp.R b c -> ηPar.R a c.
+Proof. induction 2; hauto l:on use:IO_merge. Qed.
+
+
+Lemma ηO_commute a b c :
+  ηPar.R a b -> OExp.R a c ->
+  exists d, OExp.R b d /\ ηPar.R c d.
+Proof.
+  hauto lq:on inv:OExp.R ctrs:OExp.R,ηPar.R use:ηPar.renaming, ηPar.refl.
+Qed.
+
+Lemma βO_commute a b c :
+  βPar.R a b -> OExp.R a c ->
+  exists d, OExp.R b d /\ βPar.R c d.
+Proof.
+  hauto lq:on inv:OExp.R ctrs:OExp.R,βPar.R use:βPar.renaming, βPar.refl.
+Qed.
+
+
+Lemma βO_commute0 a b c :
+  βPar.R a b -> rtc OExp.R a c ->
+  exists d, rtc OExp.R b d /\ βPar.R c d.
+Proof.
+  move => + h. move : b. induction h; hauto lq:on ctrs:rtc use:βO_commute.
+Qed.
+
+Lemma ηO_commute0 a b c :
+  ηPar.R a b -> rtc OExp.R a c ->
+  exists d, rtc OExp.R b d /\ ηPar.R c d.
+Proof.
+  move => + h. move : b. induction h; hauto lq:on ctrs:rtc use:ηO_commute.
+Qed.
+
+(* Lemma βη_commute0 a b c : *)
+(*   βPar.R a b -> *)
+(*   ηPar.R a c -> *)
+(*   exists d, ηPar.R b d /\ βPar.R c d. *)
+(* Proof. *)
+(*   move => h. move : c. *)
+(*   elim  :a b /h. *)
+(*   - move => i c. move /IO_factorization. *)
+(*     move => [b [ihb0 ihb1]]. *)
+(*     elim /IPar.inv : ihb0 => //=_. *)
+(*     move => ? [*]. subst. *)
+(*     exists c. split. apply : IO_merge'; eauto. constructor. *)
+(*     apply βPar.refl. *)
+(*   - move => b0 b1 a0 a1 hb ihb ha iha u /IO_factorization. *)
+(*     move => [v [+ hv]]. *)
+(*     elim /IPar.inv => //=_. *)
+(*     move => b2 b3 a2 a3 hb2 ha2 [*]. subst. *)
+(*     rename b3 into b2. rename a3 into a2. *)
+(*     move : hb2 => {}/ihb. move => [b12 [ihb0 ihb1]]. *)
+(*     move : ha2 => {}/iha. move => [a12 [iha0 iha1]]. *)
+(*     have h2 : βPar.R (App b2 a2) (App b12 a12) by constructor. *)
+(*     move : βO_commute0 hv h2. repeat move/[apply]. *)
+(*     move => [v][h0 h1]. *)
+(*     exists v. split => //. apply : IO_merge'; eauto; by constructor. *)
+(*   - move => a0 a1 ha iha u /IO_factorization. *)
+(*     move => [v][hb0]hb1. *)
+(*     elim /IPar.inv : hb0 => //=_. *)
+(*     move => ? a2 + [*]. subst. *)
+(*     move => {}/iha. move => [a12 [ih0 ih1]]. *)
+(*     have {ih1} : βPar.R (Abs a2) (Abs a12) by constructor. *)
+(*     move : βO_commute0 hb1. repeat move/[apply]. *)
+(*     move => [d [h0 h1]]. exists d. split => //. *)
+(*     apply : IO_merge'; eauto; by constructor. *)
+(*   - move => b0 b1 a0 a1 hb ihb ha iha u /IO_factorization. *)
+(*     move => [v][hv0]hv1. *)
+(*     elim /IPar.inv : hv0 => //=_. *)
+(*     move => ? b2 ? a2 hb2 ha2 [*]. subst. *)
+(*     move /IO_factorization : hb2 => [b [h0 h1]]. *)
+(*     elim /IPar.inv : h0 => //=_. *)
+(*     move => ? b' ha' [*]. subst. *)
+(*     move : ihb ha' => /[apply]. move => [b12 [ihb0 ihb1]]. *)
+(*     move : iha ha2 => /[apply]. move => [a12 [iha0 iha1]]. *)
+
+
+  (* - move => b0 b1 a0 a1 hb ihb ha iha u. *)
+  (*   elim /ηexp.inv => //=_. *)
+  (*   + move => b2 b3 a2 hb' [*]. subst. *)
+  (*     move : ihb hb' => /[apply]. move=> [b2 [ihb0 ihb1]]. *)
+  (*     clear iha. *)
+  (*     exists (App b2 a1). *)
+  (*     split. *)
+  (*     sfirstorder use:ηexps.AppCong, rtc_refl. *)
+  (*     hauto lq:on ctrs:βPar.R  use:βPar.refl. *)
+  (*   + move => b2 ? a2 + [*]. subst. *)
+  (*     move => {}/iha {ihb} [a12 [ih0 ih1]]. *)
+
+
+(* Lemma ηβ_commute0 a b c : *)
+(*   ηPar.R a b -> *)
+(*   βPar.R a c -> *)
+(*   exists d, βPar.R b d /\ ηPar.R c d. *)
+(* Proof. *)
+(*   move => h. move : c. elim : a b /h. *)
+(*   - hauto lq:on ctrs:βPar.R, ηPar.R inv:βPar.R. *)
+(*   - move => b0 b1 a0 a1 hb ihb ha iha u. *)
+(*     elim /βPar.inv => //=_. *)
+(*     + hauto lq:on ctrs:βPar.R, ηPar.R inv:βPar.R. *)
+(*     + move => b3 b2 a3 a2 hb2 ha2 [*]. subst. *)
+(*       rename b3 into b0. *)
+(*       have {}/ihb : βPar.R (Abs b0) (Abs b2) by eauto using βPar.AbsCong. *)
+(*       move => [b12 [ihb0 ihb1]]. *)
+
+
+(*       rename b3  into b4. rename b2 into b3. rename b4 into b2. *)
+(*       move => b2 b3 a2 a3 hb2 ha2 [*]. subst. *)
+(*       rename b3 into b2. rename a3 into a2. *)
+(*       move : ihb hb2 => /[apply]. move => [b12 [ihb0 ihb1]]. *)
+(*       move : iha ha2 => /[apply]. move => [a12 [iha0 iha1]]. *)
+
+
+
 Lemma βη_commute0 a b c :
   βPar.R a b ->
   ηexp.R a c ->
@@ -347,72 +511,6 @@ Proof.
         by asimpl.
 Qed.
 
-Module IPar.
-  Inductive R : Tm -> Tm -> Prop :=
-  | VarCong i :
-    R (VarTm i) (VarTm i)
-  | AppCong b0 b1 a0 a1 :
-    ηPar.R b0 b1 ->
-    ηPar.R a0 a1 ->
-    R (App b0 a0) (App b1 a1)
-  | AbsCong a0 a1 :
-    ηPar.R a0 a1 ->
-    R (Abs a0) (Abs a1).
-  Derive Inversion inv with (forall a b, R a b).
-
-  Lemma ToηPar a b : R a b -> ηPar.R a b.
-  Proof. induction 1; hauto lq:on ctrs:ηPar.R. Qed.
-End IPar.
-
-Module OExp.
-  Inductive R : Tm -> Tm -> Prop :=
-  | AbsEta b :
-    R b (Abs (App (ren_Tm shift b) (VarTm var_zero))).
-
-  Derive Inversion inv with (forall a b, R a b).
-End OExp.
-
-Lemma ηO_commute a b c :
-  ηPar.R a b -> OExp.R a c ->
-  exists d, OExp.R b d /\ ηPar.R c d.
-Proof.
-  hauto lq:on inv:OExp.R ctrs:OExp.R,ηPar.R use:ηPar.renaming, ηPar.refl.
-Qed.
-
-Lemma ηO_commute0 a b c :
-  ηPar.R a b -> rtc OExp.R a c ->
-  exists d, rtc OExp.R b d /\ ηPar.R c d.
-Proof.
-  move => + h. move : b. induction h; hauto lq:on ctrs:rtc use:ηO_commute.
-Qed.
-
-Lemma IO_factorization a c :
-  ηPar.R a c -> exists b, IPar.R a b /\ rtc OExp.R b c.
-Proof.
-  move => h. elim : a c /h.
-  - move => i. exists (VarTm i).
-    split. constructor.
-    apply rtc_refl.
-  - move => b0 b1 a0 a1 hb [b' [ihb0 ihb1]] ha [a' [iha0 iha1]].
-    exists (App b1 a1).
-    split. apply IPar.AppCong; eauto.
-    apply rtc_refl.
-  - move => a0 a1 ha [a' [iha0 iha1]].
-    exists (Abs a1). split. by apply IPar.AbsCong.
-    apply rtc_refl.
-  - move => b0 b1 hb [b' [ihb0 ihb1]].
-    exists b'. split => //.
-    apply : rtc_r; eauto.
-    constructor.
-Qed.
-
-Lemma IO_merge a b c :
-  ηPar.R a b -> OExp.R b c -> ηPar.R a c.
-Proof. hauto lq:on inv:OExp.R ctrs:ηPar.R. Qed.
-
-Lemma IO_merge' a b c :
-  ηPar.R a b -> rtc OExp.R b c -> ηPar.R a c.
-Proof. induction 2; hauto l:on use:IO_merge. Qed.
 
 Lemma diamond a b0 b1 :
   ηPar.R a b0 -> ηPar.R a b1 -> exists c, ηPar.R b0 c /\ ηPar.R b1 c.