Consider using datatype updates

[utaal]

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
(declare-const p1 (Pair Int Int))
(declare-const p2 (Pair Int Int))
(assert (not (= p1 p2)))
(assert (= p1 ((_ update-field first) p2 1)))
(check-sat)
(get-model)

https://microsoft.github.io/z3guide/docs/theories/Datatypes

---

https://github.com/cvc5/cvc5/blob/main/NEWS.md#datatypes :

Support for generic datatype updaters ((_ update s) t u) which replaces the field specified by selector s of t by the value u.

[utaal]

This is currently work in progress by @tim-rohde: https://github.com/principled-systems/verus/tree/struct-update-refactor