1 files changed, 9 insertions, 0 deletions
diff --git a/src/Compilers/Z/Syntax/Equality.v b/src/Compilers/Z/Syntax/Equality.v
index 745b01503..b2075c49c 100644
--- a/src/Compilers/Z/Syntax/Equality.v
+++ b/src/Compilers/Z/Syntax/Equality.v
@@ -41,6 +41,12 @@ Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : bool
        => base_type_beq T1 T1' && base_type_beq T2 T2' && base_type_beq Tout Tout'
      | Opp Tin Tout, Opp Tin' Tout'
        => base_type_beq Tin Tin' && base_type_beq Tout Tout'
+     | Zselect T1 T2 T3 Tout, Zselect T1' T2' T3' Tout'
+       => base_type_beq T1 T1' && base_type_beq T2 T2' && base_type_beq T3 T3' && base_type_beq Tout Tout'
+     | AddWithCarry T1 T2 T3 Tout, AddWithCarry T1' T2' T3' Tout'
+       => base_type_beq T1 T1' && base_type_beq T2 T2' && base_type_beq T3 T3' && base_type_beq Tout Tout'
+     | AddWithGetCarry bitwidth T1 T2 T3 Tout1 Tout2, AddWithGetCarry bitwidth' T1' T2' T3' Tout1' Tout2'
+       => Z.eqb bitwidth bitwidth' && base_type_beq T1 T1' && base_type_beq T2 T2' && base_type_beq T3 T3' && base_type_beq Tout1 Tout1' && base_type_beq Tout2 Tout2'
      | OpConst _ _, _
      | Add _ _ _, _
      | Sub _ _ _, _
@@ -50,6 +56,9 @@ Definition op_beq_hetero {t1 tR t1' tR'} (f : op t1 tR) (g : op t1' tR') : bool
      | Land _ _ _, _
      | Lor _ _ _, _
      | Opp _ _, _
+     | Zselect _ _ _ _, _
+     | AddWithCarry _ _ _ _, _
+     | AddWithGetCarry _ _ _ _ _ _, _
        => false
      end%bool.