case single e     => exact e.progress_eq
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
s₁✝ s₂✝ : State α
e : s₁✝ ↓ᵢ s₂✝
⊢ s₂✝.progress = insert (Execution.Instantaneous.Step.rcn e) s₁✝.progress
no goals