simp [record_preserves_tag, ←e₁.preserves_tag, ←e₂.preserves_tag]
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).tag = s₂.tag
no goals