diff --git a/src/Language/PlutusIR/Analysis/Equality.v b/src/Language/PlutusIR/Analysis/Equality.v
index 7454934..4362648 100644
--- a/src/Language/PlutusIR/Analysis/Equality.v
+++ b/src/Language/PlutusIR/Analysis/Equality.v
@@ -170,7 +170,7 @@ Definition string_eqb_eq := String.eqb_eq.
   Bool.eqb_true_iff
 : reflection.
 Definition andb_and : forall s t, s && t = true -> s = true /\ t = true.
-Proof. debug auto with reflection. Qed.
+Proof. auto with reflection. Qed.
 
 Ltac rewrite_eqbs := repeat (
   match goal with
diff --git a/src/Language/PlutusIR/Transform/DeadCode.v b/src/Language/PlutusIR/Transform/DeadCode.v
index d07d5e3..65da054 100644
--- a/src/Language/PlutusIR/Transform/DeadCode.v
+++ b/src/Language/PlutusIR/Transform/DeadCode.v
@@ -53,7 +53,7 @@ Inductive elim : Term -> Term -> Prop :=
 
 
 with elim_bindings : list Binding -> list Binding -> Prop :=
-  | elim_bindings : forall bs bs' bsn bs'n,
+  | elim_bindings_pure : forall bs bs' bsn bs'n,
       bsn = map name_Binding bs ->
       bs'n = map name_Binding bs' ->
 
@@ -77,7 +77,7 @@ with elim_binding : Binding -> Binding -> Prop :=
       elim t t' ->
       elim_binding (TermBind s vd t) (TermBind s vd t')
 
-  | elim_binding : forall b,
+  | elim_binding_refl : forall b,
       elim_binding b b
   .
 
diff --git a/src/Language/PlutusIR/Transform/DeadCode/DecideSound.v b/src/Language/PlutusIR/Transform/DeadCode/DecideSound.v
index c12251e..95a0873 100644
--- a/src/Language/PlutusIR/Transform/DeadCode/DecideSound.v
+++ b/src/Language/PlutusIR/Transform/DeadCode/DecideSound.v
@@ -123,7 +123,7 @@ Proof with eauto with Hints_bindings.
   simpl in H.
   unfold dec_elim_Bindings in H.
   split_hypos.
-  eapply elim_bindings...
+  eapply elim_bindings_pure...
 Qed.