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