proof.txt

                          fresh(a')     fresh(s')
       (row-var) ─────────────────────────────────────────
                 s ≃ { p: a' | s' } : [s ↦ { p: a' | s' }]     q ≠ p                         a ∉ ftv(a')                            r ∉ ftv({ q: b | s' })
(row-swap) ───────────────────────────────────────────────────────────────     (uni-varl) ─────────────────      (uni-varl) ───────────────────────────────────────
           { q: b | s } ≃ { p: a' | { q: b | s' } } : [s ↦ { p: a' | s' }]                a ∼ a' : [a ↦ a']                 r ∼ { q: b | s' } : [r ↦ { q: b | s' }]
 (uni-row) ────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
                                                     { p: a | r } ∼ { q: b | s } : [r ↦ { q: b | s' }, s ↦ { p: a | s' }]

A personal exercise based on the rules of “Extensible records with scoped labels”.