case rtr      => exact e₁.rtr_congr e₂ (s.record_preserves_rtr rcn)
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).rtr = s₂.rtr
no goals