exact e.exec.deterministic f hp
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₁
a_ih✝ : State.Nontrivial s₁ → Tail s₁ s₁ → Steps s₁ tl₂ → s₁.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₁ s₁
ht : s₁.tag = tl₂.tag
f : tl₂ ↓ᵢ+ s₂
⊢ s₁ = s₂
no goals