pub open spec fn mappings_well_formed(mappings: Set<Mapping>) -> bool
{ forall |m: Mapping| #[trigger] mappings.contains(m) ==> m.inv() }
Every mapping in the set satisfies its intrinsic invariant.