diff --git a/Arm/Insts/DPSFP/Advanced_simd_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_copy.lean
index ac3abfd7..eefcab22 100644
--- a/Arm/Insts/DPSFP/Advanced_simd_copy.lean
+++ b/Arm/Insts/DPSFP/Advanced_simd_copy.lean
@@ -29,7 +29,18 @@ def dup_aux (e : Nat) (elements : Nat) (esize : Nat)
 theorem dup_aux_0_4_32 (element : BitVec 32) (result : BitVec 128) :
   dup_aux 0 4 32 element result (by omega)
   = element ++ element ++ element ++ element := by
-  sorry
+  unfold dup_aux
+  simp [minimal_theory]
+  unfold dup_aux
+  simp [minimal_theory]
+  unfold dup_aux
+  simp [minimal_theory]
+  unfold dup_aux
+  simp [minimal_theory]
+  unfold dup_aux
+  simp [minimal_theory]
+  simp [state_simp_rules]
+  bv_decide
 
 @[state_simp_rules]
 def exec_dup_element (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState :=