sui: more proofs for the stack

CoqOfRust/RecordUpdate.v

@@ -72,6 +72,8 @@ Class Setter{R E: Type}(getter: R -> E): Type :=
   set : E -> R -> R.
 
 Arguments set {R E} (getter) {Setter} (fieldUpdater) (r).
+(* Reduce when calling the [cbn] tactic *)
+Arguments set /.
 
 Global Hint Extern 1 (@Setter ?R ?E ?getter) =>
   exact_setter R getter : typeclass_instances.

CoqOfRust/core/simulations/eq.v

@@ -2,6 +2,14 @@ Module Eq.
   Class Trait (Self : Set) : Set := {
     eqb: Self -> Self -> bool
   }.
+
+  Module Valid.
+  (** An equality [equal] is valid when it decides the standard equality [=]. *)
+  Definition t {Self : Set} `{Trait Self} (domain : Self -> Prop) : Prop :=
+    forall x y,
+    domain x -> domain y ->
+    (x = y) <-> (eqb x y = true).
+  End Valid.
 End Eq.
 
 Module Notations.