Update test failinging in odd way

Author: nomeata

tests/lean/run/structuralMutual.lean

@@ -74,13 +74,14 @@ theorem B_size_eq3 : B.empty.size = 0  := rfl
 
 /--
 trace: a : A
-h : (B.other a).size = 1
+h : (B.other a).size.add 0 = 1
 ⊢ a.size = 0
 -/
 #guard_msgs in
 theorem ex1 (a : A) (h : (A.other (B.other a)).size = 2) : a.size = 0 := by
   injection h with h
   trace_state -- without smart unfolding the state would be a mess
+  dsimp [Nat.add_zero] at h
   injection h with h
 
 -- And it computes in type just fine